# HG changeset patch # User wenzelm # Date 1394661470 -3600 # Node ID 31e427387ab5c551518367291ac2df655ecea43c # Parent 2ffdedb0c04472beff51993fc247a45cb5a126e6 tuned signature -- clarified module name; diff -r 2ffdedb0c044 -r 31e427387ab5 NEWS --- a/NEWS Wed Mar 12 22:44:55 2014 +0100 +++ b/NEWS Wed Mar 12 22:57:50 2014 +0100 @@ -437,9 +437,10 @@ theory merge). Note that the softer Thm.eq_thm_prop is often more appropriate than Thm.eq_thm. -* Simplified programming interface to define ML antiquotations, see -ML_Context.antiquotation, to make it more close to the analogous -Thy_Output.antiquotation. Minor INCOMPATIBILTY. +* Simplified programming interface to define ML antiquotations (to +make it more close to the analogous Thy_Output.antiquotation). See +ML_Context.antiquotation and structure ML_Antiquotation. Minor +INCOMPATIBILITY. * ML antiquotation @{here} refers to its source position, which is occasionally useful for experimentation and diagnostic purposes. diff -r 2ffdedb0c044 -r 31e427387ab5 src/HOL/ex/Cartouche_Examples.thy --- a/src/HOL/ex/Cartouche_Examples.thy Wed Mar 12 22:44:55 2014 +0100 +++ b/src/HOL/ex/Cartouche_Examples.thy Wed Mar 12 22:57:50 2014 +0100 @@ -106,7 +106,7 @@ setup -- "ML antiquotation" {* - ML_Antiquote.inline @{binding term_cartouche} + ML_Antiquotation.inline @{binding term_cartouche} (Args.context -- Scan.lift (Parse.inner_syntax Parse.cartouche) >> (fn (ctxt, s) => ML_Syntax.atomic (ML_Syntax.print_term (Syntax.read_term ctxt s)))) *} diff -r 2ffdedb0c044 -r 31e427387ab5 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Wed Mar 12 22:44:55 2014 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Wed Mar 12 22:57:50 2014 +0100 @@ -247,9 +247,9 @@ handle Toplevel.UNDEF => error "No goal present"; val _ = Theory.setup - (ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "state")) + (ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "state")) (Scan.succeed "Isar_Cmd.diag_state ML_context") #> - ML_Antiquote.value (Binding.qualify true "Isar" (Binding.name "goal")) + ML_Antiquotation.value (Binding.qualify true "Isar" (Binding.name "goal")) (Scan.succeed "Isar_Cmd.diag_goal ML_context")); diff -r 2ffdedb0c044 -r 31e427387ab5 src/Pure/ML/ml_antiquotation.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/ML/ml_antiquotation.ML Wed Mar 12 22:57:50 2014 +0100 @@ -0,0 +1,224 @@ +(* Title: Pure/ML/ml_antiquotation.ML + Author: Makarius + +Convenience operations for common ML antiquotations. Miscellaneous +predefined antiquotations. +*) + +signature ML_ANTIQUOTATION = +sig + val variant: string -> Proof.context -> string * Proof.context + val inline: binding -> string context_parser -> theory -> theory + val value: binding -> string context_parser -> theory -> theory +end; + +structure ML_Antiquotation: ML_ANTIQUOTATION = +struct + +(** generic tools **) + +(* ML names *) + +val init_context = ML_Syntax.reserved |> Name.declare "ML_context"; + +structure Names = Proof_Data +( + type T = Name.context; + fun init _ = init_context; +); + +fun variant a ctxt = + let + val names = Names.get ctxt; + val (b, names') = Name.variant (Name.desymbolize false a) names; + val ctxt' = Names.put names' ctxt; + in (b, ctxt') end; + + +(* specific antiquotations *) + +fun inline name scan = + ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt)); + +fun value name scan = + ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => + let + val (a, ctxt') = variant (Binding.name_of name) ctxt; + val env = "val " ^ a ^ " = " ^ s ^ ";\n"; + val body = "Isabelle." ^ a; + in (K (env, body), ctxt') end); + + + +(** misc antiquotations **) + +val _ = Theory.setup + (ML_Context.antiquotation (Binding.name "here") (Scan.succeed ()) + (fn src => fn () => fn ctxt => + let + val (a, ctxt') = variant "position" ctxt; + val (_, pos) = Args.name_of_src src; + val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n"; + val body = "Isabelle." ^ a; + in (K (env, body), ctxt') end) #> + + inline (Binding.name "assert") + (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> + + inline (Binding.name "make_string") (Scan.succeed ml_make_string) #> + + value (Binding.name "option") (Scan.lift (Parse.position Args.name) >> (fn (name, pos) => + (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos); + ML_Syntax.print_string name))) #> + + value (Binding.name "binding") + (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #> + + value (Binding.name "theory") + (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => + (Context_Position.report ctxt pos + (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name)); + "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name)) + || Scan.succeed "Proof_Context.theory_of ML_context") #> + + value (Binding.name "theory_context") + (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => + (Context_Position.report ctxt pos + (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name)); + "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ + ML_Syntax.print_string name))) #> + + inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #> + + inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> + inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> + inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> + + value (Binding.name "ctyp") (Args.typ >> (fn T => + "Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^ + ML_Syntax.atomic (ML_Syntax.print_typ T))) #> + + value (Binding.name "cterm") (Args.term >> (fn t => + "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^ + ML_Syntax.atomic (ML_Syntax.print_term t))) #> + + value (Binding.name "cprop") (Args.prop >> (fn t => + "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^ + ML_Syntax.atomic (ML_Syntax.print_term t))) #> + + value (Binding.name "cpat") + (Args.context -- + Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t => + "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^ + ML_Syntax.atomic (ML_Syntax.print_term t)))); + + +(* type classes *) + +fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) => + Proof_Context.read_class ctxt s + |> syn ? Lexicon.mark_class + |> ML_Syntax.print_string); + +val _ = Theory.setup + (inline (Binding.name "class") (class false) #> + inline (Binding.name "class_syntax") (class true) #> + + inline (Binding.name "sort") + (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) => + ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))); + + +(* type constructors *) + +fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) + >> (fn (ctxt, (s, pos)) => + let + val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s; + val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos); + val res = + (case try check (c, decl) of + SOME res => res + | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos)); + in ML_Syntax.print_string res end); + +val _ = Theory.setup + (inline (Binding.name "type_name") + (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> + inline (Binding.name "type_abbrev") + (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> + inline (Binding.name "nonterminal") + (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> + inline (Binding.name "type_syntax") + (type_name "type" (fn (c, _) => Lexicon.mark_type c))); + + +(* constants *) + +fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) + >> (fn (ctxt, (s, pos)) => + let + val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s; + val res = check (Proof_Context.consts_of ctxt, c) + handle TYPE (msg, _, _) => error (msg ^ Position.here pos); + in ML_Syntax.print_string res end); + +val _ = Theory.setup + (inline (Binding.name "const_name") + (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #> + inline (Binding.name "const_abbrev") + (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> + inline (Binding.name "const_syntax") + (const_name (fn (_, c) => Lexicon.mark_const c)) #> + + inline (Binding.name "syntax_const") + (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) => + if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c) + then ML_Syntax.print_string c + else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #> + + inline (Binding.name "const") + (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional + (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] + >> (fn ((ctxt, raw_c), Ts) => + let + val Const (c, _) = + Proof_Context.read_const {proper = true, strict = true} ctxt raw_c; + val consts = Proof_Context.consts_of ctxt; + val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); + val _ = length Ts <> n andalso + error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ + quote c ^ enclose "(" ")" (commas (replicate n "_"))); + val const = Const (c, Consts.instance consts (c, Ts)); + in ML_Syntax.atomic (ML_Syntax.print_term const) end))); + + +(* outer syntax *) + +fun with_keyword f = + Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) => + (f ((name, Thy_Header.the_keyword thy name), pos) + handle ERROR msg => error (msg ^ Position.here pos))); + +val _ = Theory.setup + (value (Binding.name "keyword") + (with_keyword + (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name + | ((name, SOME _), pos) => + error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #> + value (Binding.name "command_spec") + (with_keyword + (fn ((name, SOME kind), pos) => + "Keyword.command_spec " ^ ML_Syntax.atomic + ((ML_Syntax.print_pair + (ML_Syntax.print_pair ML_Syntax.print_string + (ML_Syntax.print_pair + (ML_Syntax.print_pair ML_Syntax.print_string + (ML_Syntax.print_list ML_Syntax.print_string)) + (ML_Syntax.print_list ML_Syntax.print_string))) + ML_Syntax.print_position) ((name, kind), pos)) + | ((name, NONE), pos) => + error ("Expected command keyword " ^ quote name ^ Position.here pos)))); + +end; + diff -r 2ffdedb0c044 -r 31e427387ab5 src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Wed Mar 12 22:44:55 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,223 +0,0 @@ -(* Title: Pure/ML/ml_antiquote.ML - Author: Makarius - -Common ML antiquotations. -*) - -signature ML_ANTIQUOTE = -sig - val variant: string -> Proof.context -> string * Proof.context - val inline: binding -> string context_parser -> theory -> theory - val value: binding -> string context_parser -> theory -> theory -end; - -structure ML_Antiquote: ML_ANTIQUOTE = -struct - -(** generic tools **) - -(* ML names *) - -val init_context = ML_Syntax.reserved |> Name.declare "ML_context"; - -structure Names = Proof_Data -( - type T = Name.context; - fun init _ = init_context; -); - -fun variant a ctxt = - let - val names = Names.get ctxt; - val (b, names') = Name.variant (Name.desymbolize false a) names; - val ctxt' = Names.put names' ctxt; - in (b, ctxt') end; - - -(* specific antiquotations *) - -fun inline name scan = - ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt)); - -fun value name scan = - ML_Context.antiquotation name scan (fn _ => fn s => fn ctxt => - let - val (a, ctxt') = variant (Binding.name_of name) ctxt; - val env = "val " ^ a ^ " = " ^ s ^ ";\n"; - val body = "Isabelle." ^ a; - in (K (env, body), ctxt') end); - - - -(** misc antiquotations **) - -val _ = Theory.setup - (ML_Context.antiquotation (Binding.name "here") (Scan.succeed ()) - (fn src => fn () => fn ctxt => - let - val (a, ctxt') = variant "position" ctxt; - val (_, pos) = Args.name_of_src src; - val env = "val " ^ a ^ " = " ^ ML_Syntax.print_position pos ^ ";\n"; - val body = "Isabelle." ^ a; - in (K (env, body), ctxt') end) #> - - inline (Binding.name "assert") - (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #> - - inline (Binding.name "make_string") (Scan.succeed ml_make_string) #> - - value (Binding.name "option") (Scan.lift (Parse.position Args.name) >> (fn (name, pos) => - (Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos); - ML_Syntax.print_string name))) #> - - value (Binding.name "binding") - (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #> - - value (Binding.name "theory") - (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => - (Context_Position.report ctxt pos - (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name)); - "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name)) - || Scan.succeed "Proof_Context.theory_of ML_context") #> - - value (Binding.name "theory_context") - (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (name, pos)) => - (Context_Position.report ctxt pos - (Theory.get_markup (Context.get_theory (Proof_Context.theory_of ctxt) name)); - "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^ - ML_Syntax.print_string name))) #> - - inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #> - - inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #> - inline (Binding.name "term") (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> - inline (Binding.name "prop") (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #> - - value (Binding.name "ctyp") (Args.typ >> (fn T => - "Thm.ctyp_of (Proof_Context.theory_of ML_context) " ^ - ML_Syntax.atomic (ML_Syntax.print_typ T))) #> - - value (Binding.name "cterm") (Args.term >> (fn t => - "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^ - ML_Syntax.atomic (ML_Syntax.print_term t))) #> - - value (Binding.name "cprop") (Args.prop >> (fn t => - "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^ - ML_Syntax.atomic (ML_Syntax.print_term t))) #> - - value (Binding.name "cpat") - (Args.context -- - Scan.lift Args.name_inner_syntax >> uncurry Proof_Context.read_term_pattern >> (fn t => - "Thm.cterm_of (Proof_Context.theory_of ML_context) " ^ - ML_Syntax.atomic (ML_Syntax.print_term t)))); - - -(* type classes *) - -fun class syn = Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) => - Proof_Context.read_class ctxt s - |> syn ? Lexicon.mark_class - |> ML_Syntax.print_string); - -val _ = Theory.setup - (inline (Binding.name "class") (class false) #> - inline (Binding.name "class_syntax") (class true) #> - - inline (Binding.name "sort") - (Args.context -- Scan.lift Args.name_inner_syntax >> (fn (ctxt, s) => - ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s))))); - - -(* type constructors *) - -fun type_name kind check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) - >> (fn (ctxt, (s, pos)) => - let - val Type (c, _) = Proof_Context.read_type_name {proper = true, strict = false} ctxt s; - val decl = Type.the_decl (Proof_Context.tsig_of ctxt) (c, pos); - val res = - (case try check (c, decl) of - SOME res => res - | NONE => error ("Not a " ^ kind ^ ": " ^ quote c ^ Position.here pos)); - in ML_Syntax.print_string res end); - -val _ = Theory.setup - (inline (Binding.name "type_name") - (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #> - inline (Binding.name "type_abbrev") - (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #> - inline (Binding.name "nonterminal") - (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #> - inline (Binding.name "type_syntax") - (type_name "type" (fn (c, _) => Lexicon.mark_type c))); - - -(* constants *) - -fun const_name check = Args.context -- Scan.lift (Parse.position Args.name_inner_syntax) - >> (fn (ctxt, (s, pos)) => - let - val Const (c, _) = Proof_Context.read_const {proper = true, strict = false} ctxt s; - val res = check (Proof_Context.consts_of ctxt, c) - handle TYPE (msg, _, _) => error (msg ^ Position.here pos); - in ML_Syntax.print_string res end); - -val _ = Theory.setup - (inline (Binding.name "const_name") - (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #> - inline (Binding.name "const_abbrev") - (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #> - inline (Binding.name "const_syntax") - (const_name (fn (_, c) => Lexicon.mark_const c)) #> - - inline (Binding.name "syntax_const") - (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, (c, pos)) => - if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c) - then ML_Syntax.print_string c - else error ("Unknown syntax const: " ^ quote c ^ Position.here pos))) #> - - inline (Binding.name "const") - (Args.context -- Scan.lift Args.name_inner_syntax -- Scan.optional - (Scan.lift (Args.$$$ "(") |-- Parse.enum1' "," Args.typ --| Scan.lift (Args.$$$ ")")) [] - >> (fn ((ctxt, raw_c), Ts) => - let - val Const (c, _) = - Proof_Context.read_const {proper = true, strict = true} ctxt raw_c; - val consts = Proof_Context.consts_of ctxt; - val n = length (Consts.typargs consts (c, Consts.type_scheme consts c)); - val _ = length Ts <> n andalso - error ("Constant requires " ^ string_of_int n ^ " type argument(s): " ^ - quote c ^ enclose "(" ")" (commas (replicate n "_"))); - val const = Const (c, Consts.instance consts (c, Ts)); - in ML_Syntax.atomic (ML_Syntax.print_term const) end))); - - -(* outer syntax *) - -fun with_keyword f = - Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) => - (f ((name, Thy_Header.the_keyword thy name), pos) - handle ERROR msg => error (msg ^ Position.here pos))); - -val _ = Theory.setup - (value (Binding.name "keyword") - (with_keyword - (fn ((name, NONE), _) => "Parse.$$$ " ^ ML_Syntax.print_string name - | ((name, SOME _), pos) => - error ("Expected minor keyword " ^ quote name ^ Position.here pos))) #> - value (Binding.name "command_spec") - (with_keyword - (fn ((name, SOME kind), pos) => - "Keyword.command_spec " ^ ML_Syntax.atomic - ((ML_Syntax.print_pair - (ML_Syntax.print_pair ML_Syntax.print_string - (ML_Syntax.print_pair - (ML_Syntax.print_pair ML_Syntax.print_string - (ML_Syntax.print_list ML_Syntax.print_string)) - (ML_Syntax.print_list ML_Syntax.print_string))) - ML_Syntax.print_position) ((name, kind), pos)) - | ((name, NONE), pos) => - error ("Expected command keyword " ^ quote name ^ Position.here pos)))); - -end; - diff -r 2ffdedb0c044 -r 31e427387ab5 src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Wed Mar 12 22:44:55 2014 +0100 +++ b/src/Pure/ML/ml_thms.ML Wed Mar 12 22:57:50 2014 +0100 @@ -42,7 +42,7 @@ val srcs = map (Attrib.check_src ctxt) raw_srcs; val _ = map (Attrib.attribute ctxt) srcs; val (a, ctxt') = ctxt - |> ML_Antiquote.variant "attributes" ||> put_attributes (i, srcs); + |> ML_Antiquotation.variant "attributes" ||> put_attributes (i, srcs); val ml = ("val " ^ a ^ " = ML_Thms.the_attributes ML_context " ^ string_of_int i ^ ";\n", "Isabelle." ^ a); @@ -54,7 +54,7 @@ fun thm_binding kind is_single thms ctxt = let val initial = null (get_thmss ctxt); - val (name, ctxt') = ML_Antiquote.variant kind ctxt; + val (name, ctxt') = ML_Antiquotation.variant kind ctxt; val ctxt'' = cons_thms ((name, is_single), thms) ctxt'; val ml_body = "Isabelle." ^ name; diff -r 2ffdedb0c044 -r 31e427387ab5 src/Pure/ROOT --- a/src/Pure/ROOT Wed Mar 12 22:44:55 2014 +0100 +++ b/src/Pure/ROOT Wed Mar 12 22:57:50 2014 +0100 @@ -143,7 +143,7 @@ "ML/exn_properties_polyml.ML" "ML/exn_trace_polyml-5.5.1.ML" "ML/install_pp_polyml.ML" - "ML/ml_antiquote.ML" + "ML/ml_antiquotation.ML" "ML/ml_compiler.ML" "ML/ml_compiler_polyml.ML" "ML/ml_context.ML" diff -r 2ffdedb0c044 -r 31e427387ab5 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Wed Mar 12 22:44:55 2014 +0100 +++ b/src/Pure/ROOT.ML Wed Mar 12 22:57:50 2014 +0100 @@ -233,7 +233,7 @@ (*basic proof engine*) use "Isar/proof_display.ML"; use "Isar/attrib.ML"; -use "ML/ml_antiquote.ML"; +use "ML/ml_antiquotation.ML"; use "Isar/context_rules.ML"; use "Isar/method.ML"; use "Isar/proof.ML"; diff -r 2ffdedb0c044 -r 31e427387ab5 src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Wed Mar 12 22:44:55 2014 +0100 +++ b/src/Pure/simplifier.ML Wed Mar 12 22:57:50 2014 +0100 @@ -144,7 +144,7 @@ val the_simproc = Name_Space.get o get_simprocs; val _ = Theory.setup - (ML_Antiquote.value (Binding.name "simproc") + (ML_Antiquotation.value (Binding.name "simproc") (Args.context -- Scan.lift (Parse.position Args.name) >> (fn (ctxt, name) => "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));