src/Pure/Isar/isar_cmd.ML
changeset 42243 2f998ff67d0f
parent 42242 39261908e12f
child 42247 12fe41a92cd5
--- a/src/Pure/Isar/isar_cmd.ML	Tue Apr 05 23:14:41 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Apr 06 10:59:43 2011 +0200
@@ -163,7 +163,7 @@
     val ctxt = ProofContext.init_global thy;
   in
     raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
-      Standard_Syntax.parse_ast_pattern ctxt (Sign.intern_type thy r, s)))
+      Syntax_Phases.parse_ast_pattern ctxt (Sign.intern_type thy r, s)))
   end;
 
 fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;