more formal read_root;
authorwenzelm
Sun Mar 09 17:37:34 2014 +0100 (2014-03-09 ago)
changeset 560066a4dcaf53664
parent 56005 4f4fc80b0613
child 56007 1b61dfbcf9a4
more formal read_root;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     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;
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Mar 09 17:08:31 2014 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 09 17:37:34 2014 +0100
     2.3 @@ -130,7 +130,7 @@
     2.4  
     2.5  val trans_pat =
     2.6    Scan.optional
     2.7 -    (@{keyword "("} |-- Parse.!!! (Parse.xname --| @{keyword ")"})) "logic"
     2.8 +    (@{keyword "("} |-- Parse.!!! (Parse.inner_syntax Parse.xname --| @{keyword ")"})) "logic"
     2.9      -- Parse.inner_syntax Parse.string;
    2.10  
    2.11  fun trans_arrow toks =