src/Pure/Isar/isar_cmd.ML

--- a/src/Pure/Isar/isar_cmd.ML	Sat Apr 16 13:48:45 2011 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Sat Apr 16 15:25:25 2011 +0200
@@ -162,7 +162,7 @@
     val ctxt = ProofContext.init_global thy;
   in
     raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
-      Syntax_Phases.parse_ast_pattern ctxt (Sign.intern_type thy r, s)))
+      Syntax_Phases.parse_ast_pattern ctxt (ProofContext.intern_type ctxt r, s)))
   end;
 
 fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;