--- 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.
--- 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))))
*}
--- 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"));
--- /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;
+
--- 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;
-
--- 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;
--- 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"
--- 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";
--- 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))));