# HG changeset patch # User wenzelm # Date 1365614087 -7200 # Node ID 43a3465805dd5c7e689d58d3faeb855df870d44f # Parent baefa3b461c2531f0c2a39c37853f06e743b28c2# Parent 27ecd33d3366943ef450bc9210d5fff97e062667 merged diff -r baefa3b461c2 -r 43a3465805dd NEWS --- a/NEWS Wed Apr 10 18:51:21 2013 +0200 +++ b/NEWS Wed Apr 10 19:14:47 2013 +0200 @@ -126,6 +126,9 @@ Skip_Proof.prove ~> Goal.prove_sorry Skip_Proof.prove_global ~> Goal.prove_sorry_global +* Antiquotation @{theory_context A} is similar to @{theory A}, but +presents the result as initial Proof.context. + *** System *** diff -r baefa3b461c2 -r 43a3465805dd src/Doc/IsarImplementation/Prelim.thy --- a/src/Doc/IsarImplementation/Prelim.thy Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Doc/IsarImplementation/Prelim.thy Wed Apr 10 19:14:47 2013 +0200 @@ -226,10 +226,13 @@ text %mlantiq {* \begin{matharray}{rcl} @{ML_antiquotation_def "theory"} & : & @{text ML_antiquotation} \\ + @{ML_antiquotation_def "theory_context"} & : & @{text ML_antiquotation} \\ \end{matharray} @{rail " @@{ML_antiquotation theory} nameref? + ; + @@{ML_antiquotation theory_context} nameref "} \begin{description} @@ -241,6 +244,10 @@ theory @{text "A"} of the background theory of the current context --- as abstract value. + \item @{text "@{theory_context A}"} is similar to @{text "@{theory + A}"}, but presents the result as initial @{ML_type Proof.context} + (see also @{ML Proof_Context.init_global}). + \end{description} *} diff -r baefa3b461c2 -r 43a3465805dd src/Doc/more_antiquote.ML --- a/src/Doc/more_antiquote.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Doc/more_antiquote.ML Wed Apr 10 19:14:47 2013 +0200 @@ -36,7 +36,7 @@ |> Code.equations_of_cert thy |> snd |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) - |> map (holize o no_vars ctxt o AxClass.overload thy); + |> map (holize o no_vars ctxt o Axclass.overload thy); in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end; in diff -r baefa3b461c2 -r 43a3465805dd src/FOL/FOL.thy --- a/src/FOL/FOL.thy Wed Apr 10 18:51:21 2013 +0200 +++ b/src/FOL/FOL.thy Wed Apr 10 19:14:47 2013 +0200 @@ -181,24 +181,19 @@ open Basic_Classical; *} -setup {* - ML_Antiquote.value @{binding claset} - (Scan.succeed "Cla.claset_of ML_context") -*} - setup Cla.setup (*Propositional rules*) lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI and [elim!] = conjE disjE impCE FalseE iffCE -ML {* val prop_cs = @{claset} *} +ML {* val prop_cs = claset_of @{context} *} (*Quantifier rules*) lemmas [intro!] = allI ex_ex1I and [intro] = exI and [elim!] = exE alt_ex1E and [elim] = allE -ML {* val FOL_cs = @{claset} *} +ML {* val FOL_cs = claset_of @{context} *} ML {* structure Blast = Blast diff -r baefa3b461c2 -r 43a3465805dd src/HOL/BNF/Tools/bnf_wrap_tactics.ML --- a/src/HOL/BNF/Tools/bnf_wrap_tactics.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_wrap_tactics.ML Wed Apr 10 19:14:47 2013 +0200 @@ -105,7 +105,7 @@ (rtac uexhaust THEN' EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex])]) cases)) 1; -val naked_ctxt = Proof_Context.init_global @{theory HOL}; +val naked_ctxt = @{theory_context HOL}; (* TODO: More precise "simp_thms"; get rid of "blast_tac" *) fun mk_split_tac uexhaust cases injectss distinctsss = diff -r baefa3b461c2 -r 43a3465805dd src/HOL/HOL.thy --- a/src/HOL/HOL.thy Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/HOL.thy Wed Apr 10 19:14:47 2013 +0200 @@ -844,11 +844,6 @@ open Basic_Classical; *} -setup {* - ML_Antiquote.value @{binding claset} - (Scan.succeed "Classical.claset_of ML_context") -*} - setup Classical.setup setup {* @@ -889,7 +884,7 @@ declare exE [elim!] allE [elim] -ML {* val HOL_cs = @{claset} *} +ML {* val HOL_cs = claset_of @{context} *} lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P" apply (erule swap) diff -r baefa3b461c2 -r 43a3465805dd src/HOL/HOLCF/IOA/meta_theory/Automata.thy --- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy Wed Apr 10 19:14:47 2013 +0200 @@ -400,7 +400,7 @@ ==> input_enabled (A||B)" apply (unfold input_enabled_def) apply (simp add: Let_def inputs_of_par trans_of_par) -apply (tactic "safe_tac (Proof_Context.init_global @{theory Fun})") +apply (tactic "safe_tac @{theory_context Fun}") apply (simp add: inp_is_act) prefer 2 apply (simp add: inp_is_act) diff -r baefa3b461c2 -r 43a3465805dd src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy --- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy Wed Apr 10 19:14:47 2013 +0200 @@ -298,7 +298,7 @@ let val ss = simpset_of ctxt in EVERY'[Seq_induct_tac ctxt sch defs, asm_full_simp_tac ss, - SELECT_GOAL (safe_tac (Proof_Context.init_global @{theory Fun})), + SELECT_GOAL (safe_tac @{theory_context Fun}), Seq_case_simp_tac ctxt exA, Seq_case_simp_tac ctxt exB, asm_full_simp_tac ss, diff -r baefa3b461c2 -r 43a3465805dd src/HOL/HOLCF/Tools/Domain/domain.ML --- a/src/HOL/HOLCF/Tools/Domain/domain.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Wed Apr 10 19:14:47 2013 +0200 @@ -44,7 +44,7 @@ fun add_arity ((b, sorts, mx), sort) thy : theory = thy |> Sign.add_types_global [(b, length sorts, mx)] - |> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort) + |> Axclass.axiomatize_arity (Sign.full_name thy b, sorts, sort) fun gen_add_domain (prep_sort : theory -> 'a -> sort) diff -r baefa3b461c2 -r 43a3465805dd src/HOL/HOLCF/Tools/Domain/domain_axioms.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML Wed Apr 10 19:14:47 2013 +0200 @@ -104,7 +104,7 @@ fun thy_arity (_, _, (lhsT, _)) = let val (dname, tvars) = dest_Type lhsT in (dname, map (snd o dest_TFree) tvars, @{sort pcpo}) end - val thy = fold (AxClass.axiomatize_arity o thy_arity) dom_eqns thy + val thy = fold (Axclass.axiomatize_arity o thy_arity) dom_eqns thy (* declare and axiomatize abs/rep *) val (iso_infos, thy) = diff -r baefa3b461c2 -r 43a3465805dd src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Wed Apr 10 19:14:47 2013 +0200 @@ -427,7 +427,7 @@ fun arity (vs, tbind, _, _, _) = (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"}) in - fold AxClass.axiomatize_arity (map arity doms) tmp_thy + fold Axclass.axiomatize_arity (map arity doms) tmp_thy end (* check bifiniteness of right-hand sides *) diff -r baefa3b461c2 -r 43a3465805dd src/HOL/HOLCF/Tools/cpodef.ML --- a/src/HOL/HOLCF/Tools/cpodef.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/HOLCF/Tools/cpodef.ML Wed Apr 10 19:14:47 2013 +0200 @@ -74,7 +74,7 @@ val (full_tname, Ts) = dest_Type newT val lhs_sorts = map (snd o dest_TFree) Ts val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1 - val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy + val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy (* transfer thms so that they will know about the new cpo instance *) val cpo_thms' = map (Thm.transfer thy) cpo_thms fun make thm = Drule.zero_var_indexes (thm OF cpo_thms') @@ -113,7 +113,7 @@ val (full_tname, Ts) = dest_Type newT val lhs_sorts = map (snd o dest_TFree) Ts val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1 - val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy + val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy val pcpo_thms' = map (Thm.transfer thy) pcpo_thms fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms') val Rep_strict = make @{thm typedef_Rep_strict} diff -r baefa3b461c2 -r 43a3465805dd src/HOL/Library/refute.ML --- a/src/HOL/Library/refute.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/Library/refute.ML Wed Apr 10 19:14:47 2013 +0200 @@ -695,7 +695,7 @@ val superclasses = distinct (op =) superclasses val class_axioms = maps (fn class => map (fn ax => ("<" ^ class ^ ">", Thm.prop_of ax)) - (#axioms (AxClass.get_info thy class) handle ERROR _ => [])) + (#axioms (Axclass.get_info thy class) handle ERROR _ => [])) superclasses (* replace the (at most one) schematic type variable in each axiom *) (* by the actual type 'T' *) diff -r baefa3b461c2 -r 43a3465805dd src/HOL/MicroJava/J/JTypeSafe.thy --- a/src/HOL/MicroJava/J/JTypeSafe.thy Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Wed Apr 10 19:14:47 2013 +0200 @@ -200,7 +200,7 @@ apply( simp_all) apply( tactic "ALLGOALS (REPEAT o resolve_tac [impI, allI])") apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] - THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *}) + THEN_ALL_NEW (full_simp_tac (simpset_of @{theory_context Conform}))) *}) apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])") -- "Level 7" diff -r baefa3b461c2 -r 43a3465805dd src/HOL/Nominal/nominal_atoms.ML --- a/src/HOL/Nominal/nominal_atoms.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/Nominal/nominal_atoms.ML Wed Apr 10 19:14:47 2013 +0200 @@ -311,7 +311,7 @@ (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2), HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x))); in - AxClass.define_class (Binding.name cl_name, ["HOL.type"]) [] + Axclass.define_class (Binding.name cl_name, ["HOL.type"]) [] [((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]), ((Binding.name (cl_name ^ "2"), []), [axiom2]), ((Binding.name (cl_name ^ "3"), []), [axiom3])] thy @@ -360,7 +360,7 @@ val axiom1 = HOLogic.mk_Trueprop (cfinite $ (csupp $ x)); in - AxClass.define_class (Binding.name cl_name, [pt_name]) [] + Axclass.define_class (Binding.name cl_name, [pt_name]) [] [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy end) ak_names_types thy8; @@ -410,7 +410,7 @@ (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x))); in - AxClass.define_class (Binding.name cl_name, ["HOL.type"]) [] + Axclass.define_class (Binding.name cl_name, ["HOL.type"]) [] [((Binding.name (cl_name ^ "1"), []), [ax1])] thy' end) ak_names_types thy) ak_names_types thy12; @@ -517,7 +517,7 @@ in thy' - |> AxClass.prove_arity (qu_name,[],[cls_name]) + |> Axclass.prove_arity (qu_name,[],[cls_name]) (fn _ => if ak_name = ak_name' then proof1 else proof2) end) ak_names thy) ak_names thy12d; @@ -551,15 +551,15 @@ val pt_thm_unit = pt_unit_inst; in thy - |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun) - |> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set) - |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) - |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn) - |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list) - |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod) - |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) + |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun) + |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set) + |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) + |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn) + |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list) + |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod) + |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_nprod) - |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit) + |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit) end) ak_names thy13; (******** fs_ class instances ********) @@ -592,7 +592,7 @@ val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI]; in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end) in - AxClass.prove_arity (qu_name,[],[qu_class]) (fn _ => proof) thy' + Axclass.prove_arity (qu_name,[],[qu_class]) (fn _ => proof) thy' end) ak_names thy) ak_names thy18; (* shows that *) @@ -616,12 +616,12 @@ val fs_thm_optn = fs_inst RS fs_option_inst; in thy - |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) - |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) - |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) + |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) + |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) + |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_nprod) - |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list) - |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn) + |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list) + |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn) end) ak_names thy20; (******** cp__ class instances ********) @@ -669,7 +669,7 @@ EVERY [Class.intro_classes_tac [], simp_tac simp_s 1] end)) in - AxClass.prove_arity (name,[],[cls_name]) (fn _ => proof) thy'' + Axclass.prove_arity (name,[],[cls_name]) (fn _ => proof) thy'' end) ak_names thy') ak_names thy) ak_names thy24; (* shows that *) @@ -700,13 +700,13 @@ val cp_thm_set = cp_inst RS cp_set_inst; in thy' - |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit) - |> AxClass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod) - |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list) - |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun) - |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn) - |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn) - |> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set) + |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit) + |> Axclass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod) + |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list) + |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun) + |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn) + |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn) + |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set) end) ak_names thy) ak_names thy25; (* show that discrete nominal types are permutation types, finitely *) @@ -722,7 +722,7 @@ val simp_s = HOL_basic_ss addsimps [Simpdata.mk_eq defn]; val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)]; in - AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy + Axclass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy end) ak_names; fun discrete_fs_inst discrete_ty defn = @@ -733,7 +733,7 @@ val simp_s = HOL_ss addsimps [supp_def, Collect_const, finite_emptyI, Simpdata.mk_eq defn]; val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1]; in - AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy + Axclass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy end) ak_names; fun discrete_cp_inst discrete_ty defn = @@ -744,7 +744,7 @@ val simp_s = HOL_ss addsimps [Simpdata.mk_eq defn]; val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1]; in - AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy + Axclass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy end) ak_names)) ak_names; in diff -r baefa3b461c2 -r 43a3465805dd src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Wed Apr 10 19:14:47 2013 +0200 @@ -425,7 +425,7 @@ (fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1, ALLGOALS (asm_full_simp_tac (simps ctxt))])) in - fold (fn (s, tvs) => fn thy => AxClass.prove_arity + fold (fn (s, tvs) => fn thy => Axclass.prove_arity (s, map (inter_sort thy sort o snd) tvs, [cp_class]) (fn _ => Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy) (full_new_type_names' ~~ tyvars) thy @@ -437,7 +437,7 @@ fold (fn atom => fn thy => let val pt_name = pt_class_of thy atom in - fold (fn (s, tvs) => fn thy => AxClass.prove_arity + fold (fn (s, tvs) => fn thy => Axclass.prove_arity (s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name]) (fn _ => EVERY [Class.intro_classes_tac [], @@ -618,7 +618,7 @@ val pt_class = pt_class_of thy atom; val sort = Sign.minimize_sort thy (Sign.certify_sort thy (pt_class :: map (cp_class_of thy atom) (remove (op =) atom dt_atoms))) - in AxClass.prove_arity + in Axclass.prove_arity (Sign.intern_type thy name, map (inter_sort thy sort o snd) tvs, [pt_class]) (fn ctxt => EVERY [Class.intro_classes_tac [], @@ -648,7 +648,7 @@ val cp1' = cp_inst_of thy atom1 atom2 RS cp1 in fold (fn ((((((Abs_inverse, Rep), perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy => - AxClass.prove_arity + Axclass.prove_arity (Sign.intern_type thy name, map (inter_sort thy sort o snd) tvs, [cp_class]) (fn ctxt => EVERY [Class.intro_classes_tac [], @@ -1105,7 +1105,7 @@ let val class = fs_class_of thy atom; val sort = Sign.minimize_sort thy (Sign.certify_sort thy (class :: pt_cp_sort)); - in fold (fn Type (s, Ts) => AxClass.prove_arity + in fold (fn Type (s, Ts) => Axclass.prove_arity (s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class]) (fn _ => Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy end) (atoms ~~ finite_supp_thms) ||> diff -r baefa3b461c2 -r 43a3465805dd src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Apr 10 19:14:47 2013 +0200 @@ -19,7 +19,7 @@ fun mk_constr_consts thy vs tyco cos = let val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos; - val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs; + val cs' = map (fn c_ty as (_, ty) => (Axclass.unoverload_const thy c_ty, ty)) cs; in if is_some (try (Code.constrset_of_consts thy) cs') then SOME cs @@ -54,7 +54,7 @@ |> Raw_Simplifier.rewrite_rule [Thm.symmetric (Thm.assume asm)] |> Thm.implies_intr asm |> Thm.generalize ([], params) 0 - |> AxClass.unoverload thy + |> Axclass.unoverload thy |> Thm.varifyT_global end; diff -r baefa3b461c2 -r 43a3465805dd src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Wed Apr 10 19:14:47 2013 +0200 @@ -1028,7 +1028,7 @@ let val supers = Sign.complete_sort thy S val class_axioms = - maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms + maps (fn class => map prop_of (Axclass.get_info thy class |> #axioms handle ERROR _ => [])) supers val monomorphic_class_axioms = map (fn t => case Term.add_tvars t [] of diff -r baefa3b461c2 -r 43a3465805dd src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Wed Apr 10 19:14:47 2013 +0200 @@ -36,7 +36,7 @@ ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs |> space_implode "\n" |> tracing else () -fun overload_const thy s = the_default s (Option.map fst (AxClass.inst_of_param thy s)) +fun overload_const thy s = the_default s (Option.map fst (Axclass.inst_of_param thy s)) fun map_specs f specs = map (fn (s, ths) => (s, f ths)) specs @@ -109,7 +109,7 @@ val intross5 = map_specs (map (remove_equalities thy2)) intross4 val _ = print_intross options thy2 "After removing equality premises:" intross5 val intross6 = - map (fn (s, ths) => (overload_const thy2 s, map (AxClass.overload thy2) ths)) intross5 + map (fn (s, ths) => (overload_const thy2 s, map (Axclass.overload thy2) ths)) intross5 val intross7 = map_specs (map (expand_tuples thy2)) intross6 val intross8 = map_specs (map (eta_contract_ho_arguments thy2)) intross7 val _ = case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ()) diff -r baefa3b461c2 -r 43a3465805dd src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Wed Apr 10 19:14:47 2013 +0200 @@ -189,7 +189,7 @@ fun get_specification options thy t = let (*val (c, T) = dest_Const t - val t = Const (AxClass.unoverload_const thy (c, T), T)*) + val t = Const (Axclass.unoverload_const thy (c, T), T)*) val _ = if show_steps options then tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^ " with type " ^ Syntax.string_of_typ_global thy (fastype_of t)) diff -r baefa3b461c2 -r 43a3465805dd src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Wed Apr 10 19:14:47 2013 +0200 @@ -93,7 +93,7 @@ val ty = Type (tyco, map TFree vs); val cs = (map o apsnd o apsnd o map o map_atyps) (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; - val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco); + val const = Axclass.param_of_inst thy (@{const_name partial_term_of}, tyco); val var_insts = map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global) [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Narrowing_variable p tt"}, diff -r baefa3b461c2 -r 43a3465805dd src/HOL/Tools/code_evaluation.ML --- a/src/HOL/Tools/code_evaluation.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/Tools/code_evaluation.ML Wed Apr 10 19:14:47 2013 +0200 @@ -78,7 +78,7 @@ val ty = Type (tyco, map TFree vs); val cs = (map o apsnd o apsnd o map o map_atyps) (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; - val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); + val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco); val eqs = map (mk_term_of_eq thy ty) cs; in thy @@ -115,7 +115,7 @@ val ty = Type (tyco, map TFree vs); val ty_rep = map_atyps (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep; - val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); + val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco); val eq = mk_abs_term_of_eq thy ty abs ty_rep proj; in thy @@ -169,7 +169,7 @@ fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t; -fun term_of_const_for thy = AxClass.unoverload_const thy o dest_Const o HOLogic.term_of_const; +fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const; fun gen_dynamic_value dynamic_value thy t = dynamic_value cookie thy NONE I (mk_term_of t) []; @@ -204,7 +204,7 @@ fun static_conv thy consts Ts = let val eqs = "==" :: @{const_name HOL.eq} :: - map (fn T => AxClass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts; + map (fn T => Axclass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts; (*assumes particular code equations for "==" etc.*) in certify_eval thy (static_value thy consts Ts) diff -r baefa3b461c2 -r 43a3465805dd src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/Tools/record.ML Wed Apr 10 19:14:47 2013 +0200 @@ -1746,12 +1746,12 @@ THEN ALLGOALS (rtac @{thm refl}); fun mk_eq thy eq_def = Simplifier.rewrite_rule - [AxClass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject; + [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject; fun mk_eq_refl thy = @{thm equal_refl} |> Thm.instantiate ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], []) - |> AxClass.unoverload thy; + |> Axclass.unoverload thy; val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq); val ensure_exhaustive_record = ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq); diff -r baefa3b461c2 -r 43a3465805dd src/HOL/Word/WordBitwise.thy --- a/src/HOL/Word/WordBitwise.thy Wed Apr 10 18:51:21 2013 +0200 +++ b/src/HOL/Word/WordBitwise.thy Wed Apr 10 19:14:47 2013 +0200 @@ -501,7 +501,7 @@ structure Word_Bitwise_Tac = struct -val word_ss = global_simpset_of @{theory Word}; +val word_ss = simpset_of @{theory_context Word}; fun mk_nat_clist ns = List.foldr (uncurry (Thm.mk_binop @{cterm "Cons :: nat => _"})) diff -r baefa3b461c2 -r 43a3465805dd src/Provers/classical.ML --- a/src/Provers/classical.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Provers/classical.ML Wed Apr 10 19:14:47 2013 +0200 @@ -56,7 +56,6 @@ val appSWrappers: Proof.context -> wrapper val appWrappers: Proof.context -> wrapper - val global_claset_of: theory -> claset val claset_of: Proof.context -> claset val map_claset: (claset -> claset) -> Proof.context -> Proof.context val put_claset: claset -> Proof.context -> Proof.context @@ -596,7 +595,6 @@ val merge = merge_cs; ); -val global_claset_of = Claset.get o Context.Theory; val claset_of = Claset.get o Context.Proof; val rep_claset_of = rep_cs o claset_of; diff -r baefa3b461c2 -r 43a3465805dd src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Pure/Isar/class.ML Wed Apr 10 19:14:47 2013 +0200 @@ -127,7 +127,7 @@ let fun params class = let - val const_typs = (#params o AxClass.get_info thy) class; + val const_typs = (#params o Axclass.get_info thy) class; val const_names = (#consts o the_class_data thy) class; in (map o apsnd) @@ -190,7 +190,7 @@ ([Pretty.command "class", Pretty.brk 1, Pretty.mark_str (Name_Space.markup_extern ctxt class_space class), Pretty.str ":", Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @ - (case try (AxClass.get_info thy) class of + (case try (Axclass.get_info thy) class of NONE => [] | SOME {params, ...} => [Pretty.fbrk, Pretty.big_list "parameters:" (map prt_param params)]) @ @@ -263,7 +263,7 @@ | NONE => I); in thy - |> AxClass.add_classrel classrel + |> Axclass.add_classrel classrel |> Class_Data.map (Graph.add_edge (sub, sup)) |> activate_defs sub (these_defs thy diff_sort) |> add_dependency @@ -401,7 +401,7 @@ fun gen_classrel mk_prop classrel thy = let fun after_qed results = - Proof_Context.background_theory ((fold o fold) AxClass.add_classrel results); + Proof_Context.background_theory ((fold o fold) Axclass.add_classrel results); in thy |> Proof_Context.init_global @@ -411,9 +411,9 @@ in val classrel = - gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel); + gen_classrel (Logic.mk_classrel oo Axclass.cert_classrel); val classrel_cmd = - gen_classrel (Logic.mk_classrel oo AxClass.read_classrel); + gen_classrel (Logic.mk_classrel oo Axclass.read_classrel); end; (*local*) @@ -472,7 +472,7 @@ let val Instantiation {params, ...} = Instantiation.get ctxt; - val lookup_inst_param = AxClass.lookup_inst_param + val lookup_inst_param = Axclass.lookup_inst_param (Sign.consts_of (Proof_Context.theory_of ctxt)) params; fun subst (c, ty) = (case lookup_inst_param (c, ty) of @@ -505,8 +505,8 @@ (* target *) fun define_overloaded (c, U) v (b_def, rhs) = - Local_Theory.background_theory_result (AxClass.declare_overloaded (c, U) - ##>> AxClass.define_overloaded b_def (c, rhs)) + Local_Theory.background_theory_result (Axclass.declare_overloaded (c, U) + ##>> Axclass.define_overloaded b_def (c, rhs)) ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v)) ##> Local_Theory.map_contexts (K synchronize_inst_syntax); @@ -541,9 +541,9 @@ val naming = Sign.naming_of thy; val _ = if null tycos then error "At least one arity must be given" else (); - val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort); + val class_params = these_params thy (filter (can (Axclass.get_info thy)) sort); fun get_param tyco (param, (_, (c, ty))) = - if can (AxClass.param_of_inst thy) (c, tyco) + if can (Axclass.param_of_inst thy) (c, tyco) then NONE else SOME ((c, tyco), (param ^ "_" ^ Long_Name.base_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty)); val params = map_product get_param tycos class_params |> map_filter I; @@ -559,7 +559,7 @@ val improve_constraints = AList.lookup (op =) (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params); fun resort_check ctxt ts = resort_terms ctxt algebra consts improve_constraints ts; - val lookup_inst_param = AxClass.lookup_inst_param consts params; + val lookup_inst_param = Axclass.lookup_inst_param consts params; fun improve (c, ty) = (case lookup_inst_param (c, ty) of SOME (_, ty') => if Sign.typ_instance thy (ty', ty) then SOME (ty, ty') else NONE @@ -593,7 +593,7 @@ val (tycos, vs, sort) = (#arities o the_instantiation) lthy; val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos; fun after_qed' results = - Local_Theory.background_theory (fold (AxClass.add_arity o Thm.varifyT_global) results) + Local_Theory.background_theory (fold (Axclass.add_arity o Thm.varifyT_global) results) #> after_qed; in lthy @@ -630,7 +630,7 @@ val sorts = map snd vs; val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos; fun after_qed results = - Proof_Context.background_theory ((fold o fold) AxClass.add_arity results); + Proof_Context.background_theory ((fold o fold) Axclass.add_arity results); in thy |> Proof_Context.init_global @@ -645,7 +645,7 @@ val thy = Thm.theory_of_thm st; val classes = Sign.all_classes thy; val class_trivs = map (Thm.class_triv thy) classes; - val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes; + val class_intros = map_filter (try (#intro o Axclass.get_info thy)) classes; val assm_intros = all_assm_intros thy; in Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st diff -r baefa3b461c2 -r 43a3465805dd src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Pure/Isar/class_declaration.ML Wed Apr 10 19:14:47 2013 +0200 @@ -90,7 +90,7 @@ ((map_types o map_atyps) (K aT) prop), of_class_prop_concl)); val sup_of_classes = map (snd o Class.rules thy) sups; val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class); - val axclass_intro = #intro (AxClass.get_info thy class); + val axclass_intro = #intro (Axclass.get_info thy class); val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort); val tac = REPEAT (SOMEGOAL @@ -289,13 +289,13 @@ |> fst |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of); fun get_axiom thy = - (case #axioms (AxClass.get_info thy class) of + (case #axioms (Axclass.get_info thy class) of [] => NONE | [thm] => SOME thm); in thy |> add_consts class base_sort sups supparam_names global_syntax - |-> (fn (param_map, params) => AxClass.define_class (bname, supsort) + |-> (fn (param_map, params) => Axclass.define_class (bname, supsort) (map (fst o snd) params) [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)] #> snd @@ -346,7 +346,7 @@ (case Named_Target.peek lthy of SOME {target, is_class = true, ...} => target | _ => error "Not in a class target"); - val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup); + val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup); val expr = ([(sup, (("", false), Expression.Positional []))], []); val (([props], deps, export), goal_ctxt) = diff -r baefa3b461c2 -r 43a3465805dd src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Pure/Isar/code.ML Wed Apr 10 19:14:47 2013 +0200 @@ -107,7 +107,7 @@ fun string_of_const thy c = let val ctxt = Proof_Context.init_global thy in - case AxClass.inst_of_param thy c of + case Axclass.inst_of_param thy c of SOME (c, tyco) => Proof_Context.extern_const ctxt c ^ " " ^ enclose "[" "]" (Proof_Context.extern_type ctxt tyco) @@ -140,7 +140,7 @@ fun check_unoverload thy (c, ty) = let - val c' = AxClass.unoverload_const thy (c, ty); + val c' = Axclass.unoverload_const thy (c, ty); val ty_decl = Sign.the_const_type thy c'; in if typscheme_equiv (ty_decl, Logic.varifyT_global ty) @@ -375,7 +375,7 @@ fun constrset_of_consts thy consts = let - val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c + val _ = map (fn (c, _) => if (is_some o Axclass.class_of_param thy) c then error ("Is a class parameter: " ^ string_of_const thy c) else ()) consts; val raw_constructors = map (analyze_constructor thy) consts; val tyco = case distinct (op =) (map (fst o fst) raw_constructors) @@ -477,7 +477,7 @@ else bad_thm "Free type variables on right hand side of equation"; val (head, args) = strip_comb lhs; val (c, ty) = case head - of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty) + of Const (c_ty as (_, ty)) => (Axclass.unoverload_const thy c_ty, ty) | _ => bad_thm "Equation not headed by constant"; fun check _ (Abs _) = bad_thm "Abstraction on left hand side of equation" | check 0 (Var _) = () @@ -485,7 +485,7 @@ | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) | check n (Const (c_ty as (c, ty))) = if allow_pats then let - val c' = AxClass.unoverload_const thy c_ty + val c' = Axclass.unoverload_const thy c_ty in if n = (length o binder_types) ty then if allow_consts orelse is_constr thy c' then () @@ -495,7 +495,7 @@ val _ = map (check 0) args; val _ = if allow_nonlinear orelse is_linear thm then () else bad_thm "Duplicate variables on left hand side of equation"; - val _ = if (is_none o AxClass.class_of_param thy) c then () + val _ = if (is_none o Axclass.class_of_param thy) c then () else bad_thm "Overloaded constant as head in equation"; val _ = if not (is_constr thy c) then () else bad_thm "Constructor as head in equation"; @@ -557,13 +557,13 @@ fun const_typ_eqn thy thm = let val (c, ty) = head_eqn thm; - val c' = AxClass.unoverload_const thy (c, ty); + val c' = Axclass.unoverload_const thy (c, ty); (*permissive wrt. to overloaded constants!*) in (c', ty) end; fun const_eqn thy = fst o const_typ_eqn thy; -fun const_abs_eqn thy = AxClass.unoverload_const thy o dest_Const o fst o strip_comb o snd +fun const_abs_eqn thy = Axclass.unoverload_const thy o dest_Const o fst o strip_comb o snd o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of; fun mk_proj tyco vs ty abs rep = @@ -629,14 +629,14 @@ fun check_abstype_cert thy proto_thm = let - val thm = (AxClass.unoverload thy o meta_rewrite thy) proto_thm; + val thm = (Axclass.unoverload thy o meta_rewrite thy) proto_thm; val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm) handle TERM _ => bad_thm "Not an equation" | THM _ => bad_thm "Not a proper equation"; val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb) o apfst dest_Const o dest_comb) lhs handle TERM _ => bad_thm "Not an abstype certificate"; - val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c + val _ = pairself (fn c => if (is_some o Axclass.class_of_param thy) c then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep); val _ = check_decl_ty thy (abs, raw_ty); val _ = check_decl_ty thy (rep, rep_ty); @@ -714,7 +714,7 @@ let val raw_ty = Logic.unvarifyT_global (const_typ thy c); val (vs, _) = typscheme thy (c, raw_ty); - val sortargs = case AxClass.class_of_param thy c + val sortargs = case Axclass.class_of_param thy c of SOME class => [[class]] | NONE => (case get_type_of_constr_or_abstr thy c of SOME (tyco, _) => (map snd o fst o the) @@ -840,12 +840,12 @@ end; fun pretty_cert thy (cert as Equations _) = - (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd) + (map_filter (Option.map (Display.pretty_thm_global thy o Axclass.overload thy) o fst o snd) o snd o equations_of_cert thy) cert | pretty_cert thy (Projection (t, _)) = [Syntax.pretty_term_global thy (Logic.varify_types_global t)] | pretty_cert thy (Abstract (abs_thm, _)) = - [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm]; + [(Display.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm]; fun bare_thms_of_cert thy (cert as Equations _) = (map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE) @@ -881,7 +881,7 @@ (map o apfst) (Thm.transfer thy) #> perhaps (perhaps_loop (perhaps_apply functrans)) #> (map o apfst) (rewrite_eqn thy eqn_conv ss) - #> (map o apfst) (AxClass.unoverload thy) + #> (map o apfst) (Axclass.unoverload thy) #> cert_of_eqns thy c; fun get_cert thy { functrans, ss } c = @@ -895,7 +895,7 @@ | Abstr (abs_thm, tyco) => abs_thm |> Thm.transfer thy |> rewrite_eqn thy Conv.arg_conv ss - |> AxClass.unoverload thy + |> Axclass.unoverload thy |> cert_of_abs thy tyco c; @@ -1172,7 +1172,7 @@ #> (map_cases o apfst) drop_outdated_cases) end; -fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty); +fun unoverload_const_typ thy (c, ty) = (Axclass.unoverload_const thy (c, ty), ty); structure Datatype_Interpretation = Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); diff -r baefa3b461c2 -r 43a3465805dd src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Pure/Isar/isar_syn.ML Wed Apr 10 19:14:47 2013 +0200 @@ -79,13 +79,13 @@ Outer_Syntax.command @{command_spec "classes"} "declare type classes" (Scan.repeat1 (Parse.binding -- Scan.optional ((@{keyword "\"} || @{keyword "<"}) |-- Parse.!!! (Parse.list1 Parse.class)) []) - >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd)); + >> (Toplevel.theory o fold Axclass.axiomatize_class_cmd)); val _ = Outer_Syntax.command @{command_spec "classrel"} "state inclusion of type classes (axiomatic!)" (Parse.and_list1 (Parse.class -- ((@{keyword "\"} || @{keyword "<"}) |-- Parse.!!! Parse.class)) - >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd)); + >> (Toplevel.theory o Axclass.axiomatize_classrel_cmd)); val _ = Outer_Syntax.local_theory @{command_spec "default_sort"} @@ -113,7 +113,7 @@ val _ = Outer_Syntax.command @{command_spec "arities"} "state type arities (axiomatic!)" - (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd)); + (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold Axclass.axiomatize_arity_cmd)); (* consts and syntax *) diff -r baefa3b461c2 -r 43a3465805dd src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Pure/Isar/proof_context.ML Wed Apr 10 19:14:47 2013 +0200 @@ -10,6 +10,7 @@ sig val theory_of: Proof.context -> theory val init_global: theory -> Proof.context + val get_global: theory -> string -> Proof.context type mode val mode_default: mode val mode_stmt: mode @@ -166,6 +167,7 @@ val theory_of = Proof_Context.theory_of; val init_global = Proof_Context.init_global; +val get_global = Proof_Context.get_global; diff -r baefa3b461c2 -r 43a3465805dd src/Pure/Isar/typedecl.ML --- a/src/Pure/Isar/typedecl.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Pure/Isar/typedecl.ML Wed Apr 10 19:14:47 2013 +0200 @@ -29,7 +29,7 @@ fun object_logic_arity name thy = (case Object_Logic.get_base_sort thy of NONE => thy - | SOME S => AxClass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy); + | SOME S => Axclass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy); fun basic_decl decl (b, n, mx) lthy = let val name = Local_Theory.full_name lthy b in diff -r baefa3b461c2 -r 43a3465805dd src/Pure/ML/ml_antiquote.ML --- a/src/Pure/ML/ml_antiquote.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Pure/ML/ml_antiquote.ML Wed Apr 10 19:14:47 2013 +0200 @@ -76,6 +76,12 @@ "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.theory -- Scan.lift (Parse.position Args.name) >> (fn (thy, (name, pos)) => + (Position.report pos (Theory.get_markup (Context.get_theory thy 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)) #> diff -r baefa3b461c2 -r 43a3465805dd src/Pure/axclass.ML --- a/src/Pure/axclass.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Pure/axclass.ML Wed Apr 10 19:14:47 2013 +0200 @@ -5,7 +5,7 @@ parameters. Proven class relations and type arities. *) -signature AX_CLASS = +signature AXCLASS = sig type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list} val get_info: theory -> class -> info @@ -38,7 +38,7 @@ val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory end; -structure AxClass: AX_CLASS = +structure Axclass: AXCLASS = struct (** theory data **) diff -r baefa3b461c2 -r 43a3465805dd src/Pure/context.ML --- a/src/Pure/context.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Pure/context.ML Wed Apr 10 19:14:47 2013 +0200 @@ -21,6 +21,7 @@ sig val theory_of: Proof.context -> theory val init_global: theory -> Proof.context + val get_global: theory -> string -> Proof.context end end; @@ -504,6 +505,7 @@ struct val theory_of = theory_of_proof; fun init_global thy = Proof.Context (init_data thy, check_thy thy); + fun get_global thy name = init_global (get_theory thy name); end; structure Proof_Data = diff -r baefa3b461c2 -r 43a3465805dd src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Pure/simplifier.ML Wed Apr 10 19:14:47 2013 +0200 @@ -10,7 +10,6 @@ include BASIC_RAW_SIMPLIFIER val map_simpset: (simpset -> simpset) -> Proof.context -> Proof.context val simpset_of: Proof.context -> simpset - val global_simpset_of: theory -> simpset val Addsimprocs: simproc list -> unit val Delsimprocs: simproc list -> unit val simp_tac: simpset -> int -> tactic @@ -169,8 +168,6 @@ (* global simpset *) fun map_simpset_global f = Context.theory_map (map_ss f); -fun global_simpset_of thy = - Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy)); fun Addsimprocs args = Context.>> (map_ss (fn ss => ss addsimprocs args)); fun Delsimprocs args = Context.>> (map_ss (fn ss => ss delsimprocs args)); diff -r baefa3b461c2 -r 43a3465805dd src/Tools/Code/code_preproc.ML --- a/src/Tools/Code/code_preproc.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Tools/Code/code_preproc.ML Wed Apr 10 19:14:47 2013 +0200 @@ -143,7 +143,7 @@ val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy; in Simplifier.rewrite pre - #> trans_conv_rule (AxClass.unoverload_conv thy) + #> trans_conv_rule (Axclass.unoverload_conv thy) end; fun preprocess_term thy = term_of_conv_resubst thy (preprocess_conv thy); @@ -152,7 +152,7 @@ let val post = (Simplifier.global_context thy o #post o the_thmproc) thy; in - AxClass.overload_conv thy + Axclass.overload_conv thy #> trans_conv_rule (Simplifier.rewrite post) end; @@ -213,14 +213,14 @@ (* auxiliary *) -fun is_proper_class thy = can (AxClass.get_info thy); +fun is_proper_class thy = can (Axclass.get_info thy); fun complete_proper_sort thy = Sign.complete_sort thy #> filter (is_proper_class thy); fun inst_params thy tyco = - map (fn (c, _) => AxClass.param_of_inst thy (c, tyco)) - o maps (#params o AxClass.get_info thy); + map (fn (c, _) => Axclass.param_of_inst thy (c, tyco)) + o maps (#params o Axclass.get_info thy); (* data structures *) diff -r baefa3b461c2 -r 43a3465805dd src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Tools/Code/code_target.ML Wed Apr 10 19:14:47 2013 +0200 @@ -544,7 +544,7 @@ fun cert_class thy class = let - val _ = AxClass.get_info thy class; + val _ = Axclass.get_info thy class; in class end; fun read_class thy = cert_class thy o Sign.intern_class thy; diff -r baefa3b461c2 -r 43a3465805dd src/Tools/Code/code_thingol.ML --- a/src/Tools/Code/code_thingol.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Tools/Code/code_thingol.ML Wed Apr 10 19:14:47 2013 +0200 @@ -269,10 +269,10 @@ local fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy); fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy); - fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst + fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy inst of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst)) | thyname :: _ => thyname; - fun thyname_of_const thy c = case AxClass.class_of_param thy c + fun thyname_of_const thy c = case Axclass.class_of_param thy c of SOME class => thyname_of_class thy class | NONE => (case Code.get_type_of_constr_or_abstr thy c of SOME (tyco, _) => thyname_of_type thy tyco @@ -662,14 +662,14 @@ end; val stmt_const = case Code.get_type_of_constr_or_abstr thy c of SOME (tyco, _) => stmt_datatypecons tyco - | NONE => (case AxClass.class_of_param thy c + | NONE => (case Axclass.class_of_param thy c of SOME class => stmt_classparam class | NONE => stmt_fun (Code_Preproc.cert eqngr c)) in ensure_stmt lookup_const (declare_const thy) stmt_const c end and ensure_class thy (algbr as (_, algebra)) eqngr permissive class = let val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; - val cs = #params (AxClass.get_info thy class); + val cs = #params (Axclass.get_info thy class); val stmt_class = fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes @@ -687,7 +687,7 @@ and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) = let val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class; - val these_class_params = these o try (#params o AxClass.get_info thy); + val these_class_params = these o try (#params o Axclass.get_info thy); val class_params = these_class_params class; val superclass_params = maps these_class_params ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class); @@ -706,7 +706,7 @@ fun translate_classparam_instance (c, ty) = let val raw_const = Const (c, map_type_tfree (K arity_typ') ty); - val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy raw_const); + val thm = Axclass.unoverload_conv thy (Thm.cterm_of thy raw_const); val const = (apsnd Logic.unvarifyT_global o dest_Const o snd o Logic.dest_equals o Thm.prop_of) thm; in diff -r baefa3b461c2 -r 43a3465805dd src/Tools/nbe.ML --- a/src/Tools/nbe.ML Wed Apr 10 18:51:21 2013 +0200 +++ b/src/Tools/nbe.ML Wed Apr 10 19:14:47 2013 +0200 @@ -56,7 +56,7 @@ of SOME T_class => T_class | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm); val tvar = case try Term.dest_TVar T - of SOME (tvar as (_, sort)) => if null (filter (can (AxClass.get_info thy)) sort) + of SOME (tvar as (_, sort)) => if null (filter (can (Axclass.get_info thy)) sort) then tvar else error ("Bad sort: " ^ Display.string_of_thm_global thy thm) | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm); @@ -65,11 +65,11 @@ val lhs_rhs = case try Logic.dest_equals eqn of SOME lhs_rhs => lhs_rhs | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn); - val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs + val c_c' = case try (pairself (Axclass.unoverload_const thy o dest_Const)) lhs_rhs of SOME c_c' => c_c' | _ => error ("Not an equation with two constants: " ^ Syntax.string_of_term_global thy eqn); - val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then () + val _ = if the_list (Axclass.class_of_param thy (snd c_c')) = [class] then () else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm); in Triv_Class_Data.map (AList.update (op =) (class, thm)) thy end; diff -r baefa3b461c2 -r 43a3465805dd src/ZF/IntDiv_ZF.thy --- a/src/ZF/IntDiv_ZF.thy Wed Apr 10 18:51:21 2013 +0200 +++ b/src/ZF/IntDiv_ZF.thy Wed Apr 10 19:14:47 2013 +0200 @@ -1712,7 +1712,7 @@ (if ~b | #0 $<= integ_of w then integ_of v zdiv (integ_of w) else (integ_of v $+ #1) zdiv (integ_of w))" - apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT) + apply (simp_tac (simpset_of @{theory_context Int} add: zadd_assoc integ_of_BIT) apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zdiv_zmult_zmult1 pos_zdiv_mult_2 lemma neg_zdiv_mult_2) done @@ -1758,7 +1758,7 @@ then #2 $* (integ_of v zmod integ_of w) $+ #1 else #2 $* ((integ_of v $+ #1) zmod integ_of w) - #1 else #2 $* (integ_of v zmod integ_of w))" - apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT) + apply (simp_tac (simpset_of @{theory_context Int} add: zadd_assoc integ_of_BIT) apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zmod_zmult_zmult1 pos_zmod_mult_2 lemma neg_zmod_mult_2) done