src/Pure/Isar/isar_cmd.ML
changeset 56006 6a4dcaf53664
parent 56005 4f4fc80b0613
child 56072 31e427387ab5
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Mar 09 17:08:31 2014 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Mar 09 17:37:34 2014 +0100
     1.3 @@ -120,9 +120,11 @@
     1.4  fun read_trrules thy raw_rules =
     1.5    let
     1.6      val ctxt = Proof_Context.init_global thy;
     1.7 +    val read_root =
     1.8 +      #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = false} ctxt;
     1.9    in
    1.10 -    raw_rules |> map (Syntax.map_trrule (fn (r, s) =>
    1.11 -      Syntax_Phases.parse_ast_pattern ctxt (Proof_Context.intern_type ctxt r, s)))
    1.12 +    raw_rules
    1.13 +    |> map (Syntax.map_trrule (fn (r, s) => Syntax_Phases.parse_ast_pattern ctxt (read_root r, s)))
    1.14    end;
    1.15  
    1.16  fun translations args thy = Sign.add_trrules (read_trrules thy args) thy;