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;