more formal read_root;

--- 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;

--- 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 =