--- a/src/Pure/Isar/attrib.ML Sun Apr 06 15:38:54 2014 +0200
+++ b/src/Pure/Isar/attrib.ML Sun Apr 06 15:43:45 2014 +0200
@@ -190,7 +190,8 @@
fun internal att = Args.src ("Pure.attribute", Position.none) [Token.mk_attribute att];
val _ = Theory.setup
- (setup (Binding.name "attribute") (Scan.lift Args.internal_attribute >> Morphism.form)
+ (setup (Binding.make ("attribute", @{here}))
+ (Scan.lift Args.internal_attribute >> Morphism.form)
"internal attribute");
--- a/src/Pure/ML/ml_antiquotation.ML Sun Apr 06 15:38:54 2014 +0200
+++ b/src/Pure/ML/ml_antiquotation.ML Sun Apr 06 15:43:45 2014 +0200
@@ -58,7 +58,7 @@
(* basic antiquotations *)
val _ = Theory.setup
- (declaration (Binding.name "here") (Scan.succeed ())
+ (declaration (Binding.make ("here", @{here})) (Scan.succeed ())
(fn src => fn () => fn ctxt =>
let
val (a, ctxt') = variant "position" ctxt;
@@ -67,7 +67,7 @@
val body = "Isabelle." ^ a;
in (K (env, body), ctxt') end) #>
- value (Binding.name "binding")
+ value (Binding.make ("binding", @{here}))
(Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding));
end;
--- a/src/Pure/Proof/extraction.ML Sun Apr 06 15:38:54 2014 +0200
+++ b/src/Pure/Proof/extraction.ML Sun Apr 06 15:43:45 2014 +0200
@@ -36,12 +36,14 @@
val add_syntax =
Sign.root_path
- #> Sign.add_types_global [(Binding.name "Type", 0, NoSyn), (Binding.name "Null", 0, NoSyn)]
+ #> Sign.add_types_global
+ [(Binding.make ("Type", @{here}), 0, NoSyn),
+ (Binding.make ("Null", @{here}), 0, NoSyn)]
#> Sign.add_consts
- [(Binding.name "typeof", typ "'b => Type", NoSyn),
- (Binding.name "Type", typ "'a itself => Type", NoSyn),
- (Binding.name "Null", typ "Null", NoSyn),
- (Binding.name "realizes", typ "'a => 'b => 'b", NoSyn)];
+ [(Binding.make ("typeof", @{here}), typ "'b => Type", NoSyn),
+ (Binding.make ("Type", @{here}), typ "'a itself => Type", NoSyn),
+ (Binding.make ("Null", @{here}), typ "Null", NoSyn),
+ (Binding.make ("realizes", @{here}), typ "'a => 'b => 'b", NoSyn)];
val nullT = Type ("Null", []);
val nullt = Const ("Null", nullT);
--- a/src/Pure/Proof/proof_syntax.ML Sun Apr 06 15:38:54 2014 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Sun Apr 06 15:43:45 2014 +0200
@@ -43,44 +43,47 @@
thy
|> Sign.root_path
|> Sign.set_defsort []
- |> Sign.add_types_global [(Binding.name "proof", 0, NoSyn)]
+ |> Sign.add_types_global
+ [(Binding.make ("proof", @{here}), 0, NoSyn)]
|> fold (snd oo Sign.declare_const_global)
- [((Binding.name "Appt", [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)),
- ((Binding.name "AppP", [proofT, proofT] ---> proofT), Mixfix ("(1_ %%/ _)", [4, 5], 4)),
- ((Binding.name "Abst", (aT --> proofT) --> proofT), NoSyn),
- ((Binding.name "AbsP", [propT, proofT --> proofT] ---> proofT), NoSyn),
- ((Binding.name "Hyp", propT --> proofT), NoSyn),
- ((Binding.name "Oracle", propT --> proofT), NoSyn),
- ((Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT), NoSyn),
- ((Binding.name "MinProof", proofT), Delimfix "?")]
- |> Sign.add_nonterminals_global [Binding.name "param", Binding.name "params"]
+ [((Binding.make ("Appt", @{here}), [proofT, aT] ---> proofT), Mixfix ("(1_ %/ _)", [4, 5], 4)),
+ ((Binding.make ("AppP", @{here}), [proofT, proofT] ---> proofT), Mixfix ("(1_ %%/ _)", [4, 5], 4)),
+ ((Binding.make ("Abst", @{here}), (aT --> proofT) --> proofT), NoSyn),
+ ((Binding.make ("AbsP", @{here}), [propT, proofT --> proofT] ---> proofT), NoSyn),
+ ((Binding.make ("Hyp", @{here}), propT --> proofT), NoSyn),
+ ((Binding.make ("Oracle", @{here}), propT --> proofT), NoSyn),
+ ((Binding.make ("OfClass", @{here}), (Term.a_itselfT --> propT) --> proofT), NoSyn),
+ ((Binding.make ("MinProof", @{here}), proofT), Delimfix "?")]
+ |> Sign.add_nonterminals_global
+ [Binding.make ("param", @{here}),
+ Binding.make ("params", @{here})]
|> Sign.add_syntax Syntax.mode_default
- [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
- ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
- ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
- ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),
- ("", paramT --> paramT, Delimfix "'(_')"),
- ("", idtT --> paramsT, Delimfix "_"),
- ("", paramT --> paramsT, Delimfix "_")]
+ [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)),
+ ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
+ ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)),
+ ("_Lam1", [idtT, propT] ---> paramT, Mixfix ("_: _", [0, 0], 0)),
+ ("", paramT --> paramT, Delimfix "'(_')"),
+ ("", idtT --> paramsT, Delimfix "_"),
+ ("", paramT --> paramsT, Delimfix "_")]
|> Sign.add_syntax (Symbol.xsymbolsN, true)
- [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
- (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
- (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]
+ [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
+ (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
+ (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]
|> Sign.add_trrules (map Syntax.Parse_Print_Rule
- [(Ast.mk_appl (Ast.Constant "_Lam")
- [Ast.mk_appl (Ast.Constant "_Lam0")
- [Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"],
- Ast.mk_appl (Ast.Constant "_Lam")
- [Ast.Variable "l",
- Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]),
- (Ast.mk_appl (Ast.Constant "_Lam")
- [Ast.mk_appl (Ast.Constant "_Lam1")
- [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
- Ast.mk_appl (Ast.Constant (Lexicon.mark_const "AbsP")) [Ast.Variable "A",
- (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
- (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
- Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Abst"))
- [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
+ [(Ast.mk_appl (Ast.Constant "_Lam")
+ [Ast.mk_appl (Ast.Constant "_Lam0")
+ [Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"],
+ Ast.mk_appl (Ast.Constant "_Lam")
+ [Ast.Variable "l",
+ Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "m", Ast.Variable "A"]]),
+ (Ast.mk_appl (Ast.Constant "_Lam")
+ [Ast.mk_appl (Ast.Constant "_Lam1")
+ [Ast.Variable "x", Ast.Variable "A"], Ast.Variable "B"],
+ Ast.mk_appl (Ast.Constant (Lexicon.mark_const "AbsP")) [Ast.Variable "A",
+ (Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "B"])]),
+ (Ast.mk_appl (Ast.Constant "_Lam") [Ast.Variable "x", Ast.Variable "A"],
+ Ast.mk_appl (Ast.Constant (Lexicon.mark_const "Abst"))
+ [(Ast.mk_appl (Ast.Constant "_abs") [Ast.Variable "x", Ast.Variable "A"])])]);
(**** translation between proof terms and pure terms ****)
--- a/src/Pure/conjunction.ML Sun Apr 06 15:38:54 2014 +0200
+++ b/src/Pure/conjunction.ML Sun Apr 06 15:43:45 2014 +0200
@@ -84,11 +84,14 @@
in
-val conjunctionD1 = Drule.store_standard_thm (Binding.name "conjunctionD1") (conjunctionD #1);
-val conjunctionD2 = Drule.store_standard_thm (Binding.name "conjunctionD2") (conjunctionD #2);
+val conjunctionD1 =
+ Drule.store_standard_thm (Binding.make ("conjunctionD1", @{here})) (conjunctionD #1);
+
+val conjunctionD2 =
+ Drule.store_standard_thm (Binding.make ("conjunctionD2", @{here})) (conjunctionD #2);
val conjunctionI =
- Drule.store_standard_thm (Binding.name "conjunctionI")
+ Drule.store_standard_thm (Binding.make ("conjunctionI", @{here}))
(Drule.implies_intr_list [A, B]
(Thm.equal_elim
(Thm.symmetric conjunction_def)
--- a/src/Pure/drule.ML Sun Apr 06 15:38:54 2014 +0200
+++ b/src/Pure/drule.ML Sun Apr 06 15:43:45 2014 +0200
@@ -385,13 +385,13 @@
val reflexive_thm =
let val cx = certify (Var(("x",0),TVar(("'a",0),[])))
- in store_standard_thm_open (Binding.name "reflexive") (Thm.reflexive cx) end;
+ in store_standard_thm_open (Binding.make ("reflexive", @{here})) (Thm.reflexive cx) end;
val symmetric_thm =
let
val xy = read_prop "x::'a == y::'a";
val thm = Thm.implies_intr xy (Thm.symmetric (Thm.assume xy));
- in store_standard_thm_open (Binding.name "symmetric") thm end;
+ in store_standard_thm_open (Binding.make ("symmetric", @{here})) thm end;
val transitive_thm =
let
@@ -400,7 +400,7 @@
val xythm = Thm.assume xy;
val yzthm = Thm.assume yz;
val thm = Thm.implies_intr yz (Thm.transitive xythm yzthm);
- in store_standard_thm_open (Binding.name "transitive") thm end;
+ in store_standard_thm_open (Binding.make ("transitive", @{here})) thm end;
fun extensional eq =
let val eq' =
@@ -408,7 +408,7 @@
in Thm.equal_elim (Thm.eta_conversion (cprop_of eq')) eq' end;
val equals_cong =
- store_standard_thm_open (Binding.name "equals_cong")
+ store_standard_thm_open (Binding.make ("equals_cong", @{here}))
(Thm.reflexive (read_prop "x::'a == y::'a"));
val imp_cong =
@@ -418,13 +418,14 @@
val AC = read_prop "A ==> C"
val A = read_prop "A"
in
- store_standard_thm_open (Binding.name "imp_cong") (Thm.implies_intr ABC (Thm.equal_intr
- (Thm.implies_intr AB (Thm.implies_intr A
- (Thm.equal_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A))
- (Thm.implies_elim (Thm.assume AB) (Thm.assume A)))))
- (Thm.implies_intr AC (Thm.implies_intr A
- (Thm.equal_elim (Thm.symmetric (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)))
- (Thm.implies_elim (Thm.assume AC) (Thm.assume A)))))))
+ store_standard_thm_open (Binding.make ("imp_cong", @{here}))
+ (Thm.implies_intr ABC (Thm.equal_intr
+ (Thm.implies_intr AB (Thm.implies_intr A
+ (Thm.equal_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A))
+ (Thm.implies_elim (Thm.assume AB) (Thm.assume A)))))
+ (Thm.implies_intr AC (Thm.implies_intr A
+ (Thm.equal_elim (Thm.symmetric (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)))
+ (Thm.implies_elim (Thm.assume AC) (Thm.assume A)))))))
end;
val swap_prems_eq =
@@ -434,7 +435,7 @@
val A = read_prop "A"
val B = read_prop "B"
in
- store_standard_thm_open (Binding.name "swap_prems_eq")
+ store_standard_thm_open (Binding.make ("swap_prems_eq", @{here}))
(Thm.equal_intr
(Thm.implies_intr ABC (Thm.implies_intr B (Thm.implies_intr A
(Thm.implies_elim (Thm.implies_elim (Thm.assume ABC) (Thm.assume A)) (Thm.assume B)))))
@@ -504,11 +505,13 @@
(*** Some useful meta-theorems ***)
(*The rule V/V, obtains assumption solving for eresolve_tac*)
-val asm_rl = store_standard_thm_open (Binding.name "asm_rl") (Thm.trivial (read_prop "?psi"));
+val asm_rl =
+ store_standard_thm_open (Binding.make ("asm_rl", @{here}))
+ (Thm.trivial (read_prop "?psi"));
(*Meta-level cut rule: [| V==>W; V |] ==> W *)
val cut_rl =
- store_standard_thm_open (Binding.name "cut_rl")
+ store_standard_thm_open (Binding.make ("cut_rl", @{here}))
(Thm.trivial (read_prop "?psi ==> ?theta"));
(*Generalized elim rule for one conclusion; cut_rl with reversed premises:
@@ -518,8 +521,9 @@
val V = read_prop "V";
val VW = read_prop "V ==> W";
in
- store_standard_thm_open (Binding.name "revcut_rl")
- (Thm.implies_intr V (Thm.implies_intr VW (Thm.implies_elim (Thm.assume VW) (Thm.assume V))))
+ store_standard_thm_open (Binding.make ("revcut_rl", @{here}))
+ (Thm.implies_intr V
+ (Thm.implies_intr VW (Thm.implies_elim (Thm.assume VW) (Thm.assume V))))
end;
(*for deleting an unwanted assumption*)
@@ -528,7 +532,7 @@
val V = read_prop "V";
val W = read_prop "W";
val thm = Thm.implies_intr V (Thm.implies_intr W (Thm.assume W));
- in store_standard_thm_open (Binding.name "thin_rl") thm end;
+ in store_standard_thm_open (Binding.make ("thin_rl", @{here})) thm end;
(* (!!x. PROP ?V) == PROP ?V Allows removal of redundant parameters*)
val triv_forall_equality =
@@ -537,7 +541,7 @@
val QV = read_prop "!!x::'a. V";
val x = certify (Free ("x", Term.aT []));
in
- store_standard_thm_open (Binding.name "triv_forall_equality")
+ store_standard_thm_open (Binding.make ("triv_forall_equality", @{here}))
(Thm.equal_intr (Thm.implies_intr QV (Thm.forall_elim x (Thm.assume QV)))
(Thm.implies_intr V (Thm.forall_intr x (Thm.assume V))))
end;
@@ -550,8 +554,9 @@
val AAB = read_prop "Phi ==> Phi ==> Psi";
val A = read_prop "Phi";
in
- store_standard_thm_open (Binding.name "distinct_prems_rl")
- (implies_intr_list [AAB, A] (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A]))
+ store_standard_thm_open (Binding.make ("distinct_prems_rl", @{here}))
+ (implies_intr_list [AAB, A]
+ (implies_elim_list (Thm.assume AAB) [Thm.assume A, Thm.assume A]))
end;
(* [| PROP ?phi ==> PROP ?psi; PROP ?psi ==> PROP ?phi |]
@@ -563,8 +568,9 @@
val PQ = read_prop "phi ==> psi";
val QP = read_prop "psi ==> phi";
in
- store_standard_thm_open (Binding.name "equal_intr_rule")
- (Thm.implies_intr PQ (Thm.implies_intr QP (Thm.equal_intr (Thm.assume PQ) (Thm.assume QP))))
+ store_standard_thm_open (Binding.make ("equal_intr_rule", @{here}))
+ (Thm.implies_intr PQ
+ (Thm.implies_intr QP (Thm.equal_intr (Thm.assume PQ) (Thm.assume QP))))
end;
(* PROP ?phi == PROP ?psi ==> PROP ?phi ==> PROP ?psi *)
@@ -573,13 +579,13 @@
val eq = read_prop "phi::prop == psi::prop";
val P = read_prop "phi";
in
- store_standard_thm_open (Binding.name "equal_elim_rule1")
+ store_standard_thm_open (Binding.make ("equal_elim_rule1", @{here}))
(Thm.equal_elim (Thm.assume eq) (Thm.assume P) |> implies_intr_list [eq, P])
end;
(* PROP ?psi == PROP ?phi ==> PROP ?phi ==> PROP ?psi *)
val equal_elim_rule2 =
- store_standard_thm_open (Binding.name "equal_elim_rule2")
+ store_standard_thm_open (Binding.make ("equal_elim_rule2", @{here}))
(symmetric_thm RS equal_elim_rule1);
(* PROP ?phi ==> PROP ?phi ==> PROP ?psi ==> PROP ?psi *)
@@ -588,7 +594,7 @@
val P = read_prop "phi";
val Q = read_prop "psi";
val thm = implies_intr_list [P, P, Q] (Thm.assume Q);
- in store_standard_thm_open (Binding.name "remdups_rl") thm end;
+ in store_standard_thm_open (Binding.make ("remdups_rl", @{here})) thm end;
@@ -610,15 +616,16 @@
val protect = Thm.apply (certify Logic.protectC);
val protectI =
- store_standard_thm (Binding.conceal (Binding.name "protectI"))
+ store_standard_thm (Binding.conceal (Binding.make ("protectI", @{here})))
(Thm.equal_elim (Thm.symmetric prop_def) (Thm.assume A));
val protectD =
- store_standard_thm (Binding.conceal (Binding.name "protectD"))
+ store_standard_thm (Binding.conceal (Binding.make ("protectD", @{here})))
(Thm.equal_elim prop_def (Thm.assume (protect A)));
val protect_cong =
- store_standard_thm_open (Binding.name "protect_cong") (Thm.reflexive (protect A));
+ store_standard_thm_open (Binding.make ("protect_cong", @{here}))
+ (Thm.reflexive (protect A));
fun implies_intr_protected asms th =
let val asms' = map protect asms in
@@ -632,7 +639,7 @@
(* term *)
val termI =
- store_standard_thm (Binding.conceal (Binding.name "termI"))
+ store_standard_thm (Binding.conceal (Binding.make ("termI", @{here})))
(Thm.equal_elim (Thm.symmetric term_def) (Thm.forall_intr A (Thm.trivial A)));
fun mk_term ct =
@@ -660,11 +667,11 @@
(* sort_constraint *)
val sort_constraintI =
- store_standard_thm (Binding.conceal (Binding.name "sort_constraintI"))
+ store_standard_thm (Binding.conceal (Binding.make ("sort_constraintI", @{here})))
(Thm.equal_elim (Thm.symmetric sort_constraint_def) (mk_term T));
val sort_constraint_eq =
- store_standard_thm (Binding.conceal (Binding.name "sort_constraint_eq"))
+ store_standard_thm (Binding.conceal (Binding.make ("sort_constraint_eq", @{here})))
(Thm.equal_intr
(Thm.implies_intr CA (Thm.implies_elim (Thm.assume CA)
(Thm.unvarify_global sort_constraintI)))
@@ -699,7 +706,7 @@
|> Thm.forall_intr cx
|> Thm.implies_intr cphi
|> Thm.implies_intr rhs)
- |> store_standard_thm_open (Binding.name "norm_hhf_eq")
+ |> store_standard_thm_open (Binding.make ("norm_hhf_eq", @{here}))
end;
val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq);
--- a/src/Pure/pure_thy.ML Sun Apr 06 15:38:54 2014 +0200
+++ b/src/Pure/pure_thy.ML Sun Apr 06 15:43:45 2014 +0200
@@ -62,12 +62,12 @@
(Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
Old_Appl_Syntax.put false #>
Sign.add_types_global
- [(Binding.name "fun", 2, NoSyn),
- (Binding.name "prop", 0, NoSyn),
- (Binding.name "itself", 1, NoSyn),
- (Binding.name "dummy", 0, NoSyn)]
+ [(Binding.make ("fun", @{here}), 2, NoSyn),
+ (Binding.make ("prop", @{here}), 0, NoSyn),
+ (Binding.make ("itself", @{here}), 1, NoSyn),
+ (Binding.make ("dummy", @{here}), 0, NoSyn)]
#> Sign.add_nonterminals_global
- (map Binding.name
+ (map (fn name => Binding.make (name, @{here}))
(Lexicon.terminals @ ["logic", "type", "types", "sort", "classes",
"args", "cargs", "pttrn", "pttrns", "idt", "idts", "aprop", "asms",
"any", "prop'", "num_const", "float_const", "xnum_const", "num_position",
@@ -195,12 +195,12 @@
#> Sign.add_syntax ("HTML", false)
[("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3))]
#> Sign.add_consts
- [(qualify (Binding.name "eq"), typ "'a => 'a => prop", Infix ("==", 2)),
- (qualify (Binding.name "imp"), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
- (qualify (Binding.name "all"), typ "('a => prop) => prop", Binder ("!!", 0, 0)),
- (qualify (Binding.name "prop"), typ "prop => prop", NoSyn),
- (qualify (Binding.name "type"), typ "'a itself", NoSyn),
- (qualify (Binding.name "dummy_pattern"), typ "'a", Delimfix "'_")]
+ [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("==", 2)),
+ (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
+ (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("!!", 0, 0)),
+ (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
+ (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
+ (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]
#> Theory.add_deps_global "Pure.eq" ("Pure.eq", typ "'a => 'a => prop") []
#> Theory.add_deps_global "Pure.imp" ("Pure.imp", typ "prop => prop => prop") []
#> Theory.add_deps_global "Pure.all" ("Pure.all", typ "('a => prop) => prop") []
@@ -210,19 +210,22 @@
#> Sign.parse_translation Syntax_Trans.pure_parse_translation
#> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation
#> Sign.add_consts
- [(qualify (Binding.name "term"), typ "'a => prop", NoSyn),
- (qualify (Binding.name "sort_constraint"), typ "'a itself => prop", NoSyn),
- (qualify (Binding.name "conjunction"), typ "prop => prop => prop", NoSyn)]
+ [(qualify (Binding.make ("term", @{here})), typ "'a => prop", NoSyn),
+ (qualify (Binding.make ("sort_constraint", @{here})), typ "'a itself => prop", NoSyn),
+ (qualify (Binding.make ("conjunction", @{here})), typ "prop => prop => prop", NoSyn)]
#> Sign.local_path
#> (Global_Theory.add_defs false o map Thm.no_attributes)
- [(Binding.name "prop_def", prop "(CONST Pure.prop :: prop => prop) (A::prop) == A::prop"),
- (Binding.name "term_def", prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
- (Binding.name "sort_constraint_def",
+ [(Binding.make ("prop_def", @{here}),
+ prop "(CONST Pure.prop :: prop => prop) (A::prop) == A::prop"),
+ (Binding.make ("term_def", @{here}),
+ prop "(CONST Pure.term :: 'a => prop) (x::'a) == (!!A::prop. A ==> A)"),
+ (Binding.make ("sort_constraint_def", @{here}),
prop "(CONST Pure.sort_constraint :: 'a itself => prop) (CONST Pure.type :: 'a itself) ==\
\ (CONST Pure.term :: 'a itself => prop) (CONST Pure.type :: 'a itself)"),
- (Binding.name "conjunction_def", prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
- #> Global_Theory.add_thmss [((Binding.name "nothing", []), [])] #> snd
+ (Binding.make ("conjunction_def", @{here}),
+ prop "(A &&& B) == (!!C::prop. (A ==> B ==> C) ==> C)")] #> snd
+ #> Global_Theory.add_thmss [((Binding.make ("nothing", @{here}), []), [])] #> snd
#> fold (fn (a, prop) =>
- snd o Thm.add_axiom_global (Binding.name a, prop)) Proofterm.equality_axms);
+ snd o Thm.add_axiom_global (Binding.make (a, @{here}), prop)) Proofterm.equality_axms);
end;
--- a/src/Pure/skip_proof.ML Sun Apr 06 15:38:54 2014 +0200
+++ b/src/Pure/skip_proof.ML Sun Apr 06 15:43:45 2014 +0200
@@ -26,7 +26,8 @@
(* oracle setup *)
val (_, make_thm_cterm) =
- Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "skip_proof", I)));
+ Context.>>>
+ (Context.map_theory_result (Thm.add_oracle (Binding.make ("skip_proof", @{here}), I)));
fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop);