# HG changeset patch # User wenzelm # Date 1396791825 -7200 # Node ID 30ccec1e82fb8884ebe3b3669b92d4739559df85 # Parent 28b34e8e4a80d41951f1c7e0bdbc9dae1f0d9176 more source positions; diff -r 28b34e8e4a80 -r 30ccec1e82fb src/Pure/Isar/attrib.ML --- 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"); diff -r 28b34e8e4a80 -r 30ccec1e82fb src/Pure/ML/ml_antiquotation.ML --- 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; diff -r 28b34e8e4a80 -r 30ccec1e82fb src/Pure/Proof/extraction.ML --- 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); diff -r 28b34e8e4a80 -r 30ccec1e82fb src/Pure/Proof/proof_syntax.ML --- 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>\_./ _)", [0, 3], 3)), - (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4)), - (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4))] + [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\_./ _)", [0, 3], 3)), + (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4)), + (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \/ _)", [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 ****) diff -r 28b34e8e4a80 -r 30ccec1e82fb src/Pure/conjunction.ML --- 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) diff -r 28b34e8e4a80 -r 30ccec1e82fb src/Pure/drule.ML --- 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); diff -r 28b34e8e4a80 -r 30ccec1e82fb src/Pure/pure_thy.ML --- 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\\_./ _)", [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; diff -r 28b34e8e4a80 -r 30ccec1e82fb src/Pure/skip_proof.ML --- 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);