# HG changeset patch
# User wenzelm
# Date 1394383054 -3600
# Node ID 6a4dcaf53664252726b83c6443ce52c5f7605ce9
# Parent  4f4fc80b0613c03f7714974000d6b8b39d7f86b5
more formal read_root;

diff -r 4f4fc80b0613 -r 6a4dcaf53664 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Sun Mar 09 17:08:31 2014 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 09 17:37:34 2014 +0100
@@ -120,9 +120,11 @@
 fun read_trrules thy raw_rules =
   let
     val ctxt = Proof_Context.init_global thy;
+    val read_root =
+      #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} ctxt;
   in
-    raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
-      Syntax_Phases.parse_ast_pattern ctxt (Proof_Context.intern_type ctxt r, s)))
+    raw_rules
+    |> map (Syntax.map_trrule (fn (r, s) => Syntax_Phases.parse_ast_pattern ctxt (read_root r, s)))
   end;
 
 fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;
diff -r 4f4fc80b0613 -r 6a4dcaf53664 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Mar 09 17:08:31 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 09 17:37:34 2014 +0100
@@ -130,7 +130,7 @@
 
 val trans_pat =
   Scan.optional
-    (@{keyword "("} |-- Parse.!!! (Parse.xname --| @{keyword ")"})) "logic"
+    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
     -- Parse.inner_syntax Parse.string;
 
 fun trans_arrow toks =