X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=1fdc87b416b367861d3d6af32fb5b06247b7f769;hb=5b45f78ed4293ebbe8cc73ad925bca11a300d021;hp=9e3ea3b5a91bc8c6f299609d9d400c8b36a90f84;hpb=a57ca0d68754b946b33976acf2e72f45ff11c8d7;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 9e3ea3b5a..1fdc87b41 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -121,9 +121,11 @@ let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
   | AutoBatch (_,params) -> "autobatch " ^ 
       pp_auto_params ~term_pp params
   | Assumption _ -> "assumption"
-  | Cases (_, term, pattern, specs) -> Printf.sprintf "cases " ^ term_pp term ^
-      pp_tactic_pattern pattern ^
-      pp_intros_specs "names " specs 
+  | Cases (_, term, pattern, specs) -> 
+      Printf.sprintf "cases %s %s%s" 
+      (term_pp term)
+      (pp_tactic_pattern pattern)
+      (pp_intros_specs "names " specs)
   | Change (_, where, with_what) ->
       Printf.sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)
   | Clear (_,ids) -> Printf.sprintf "clear %s" (pp_hyps ids)