merged
authorwenzelm
Wed Apr 10 19:14:47 2013 +0200 (2013-04-10)
changeset 5168943a3465805dd
parent 51683 baefa3b461c2
parent 51688 27ecd33d3366
child 51690 c85409ead923
merged
NEWS
src/HOL/HOL.thy
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/NEWS	Wed Apr 10 18:51:21 2013 +0200
     1.2 +++ b/NEWS	Wed Apr 10 19:14:47 2013 +0200
     1.3 @@ -126,6 +126,9 @@
     1.4      Skip_Proof.prove  ~>  Goal.prove_sorry
     1.5      Skip_Proof.prove_global  ~>  Goal.prove_sorry_global
     1.6  
     1.7 +* Antiquotation @{theory_context A} is similar to @{theory A}, but
     1.8 +presents the result as initial Proof.context.
     1.9 +
    1.10  
    1.11  *** System ***
    1.12  
     2.1 --- a/src/Doc/IsarImplementation/Prelim.thy	Wed Apr 10 18:51:21 2013 +0200
     2.2 +++ b/src/Doc/IsarImplementation/Prelim.thy	Wed Apr 10 19:14:47 2013 +0200
     2.3 @@ -226,10 +226,13 @@
     2.4  text %mlantiq {*
     2.5    \begin{matharray}{rcl}
     2.6    @{ML_antiquotation_def "theory"} & : & @{text ML_antiquotation} \\
     2.7 +  @{ML_antiquotation_def "theory_context"} & : & @{text ML_antiquotation} \\
     2.8    \end{matharray}
     2.9  
    2.10    @{rail "
    2.11    @@{ML_antiquotation theory} nameref?
    2.12 +  ;
    2.13 +  @@{ML_antiquotation theory_context} nameref
    2.14    "}
    2.15  
    2.16    \begin{description}
    2.17 @@ -241,6 +244,10 @@
    2.18    theory @{text "A"} of the background theory of the current context
    2.19    --- as abstract value.
    2.20  
    2.21 +  \item @{text "@{theory_context A}"} is similar to @{text "@{theory
    2.22 +  A}"}, but presents the result as initial @{ML_type Proof.context}
    2.23 +  (see also @{ML Proof_Context.init_global}).
    2.24 +
    2.25    \end{description}
    2.26  *}
    2.27  
     3.1 --- a/src/Doc/more_antiquote.ML	Wed Apr 10 18:51:21 2013 +0200
     3.2 +++ b/src/Doc/more_antiquote.ML	Wed Apr 10 19:14:47 2013 +0200
     3.3 @@ -36,7 +36,7 @@
     3.4        |> Code.equations_of_cert thy
     3.5        |> snd
     3.6        |> map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
     3.7 -      |> map (holize o no_vars ctxt o AxClass.overload thy);
     3.8 +      |> map (holize o no_vars ctxt o Axclass.overload thy);
     3.9    in Thy_Output.output ctxt (Thy_Output.maybe_pretty_source pretty_thm ctxt src thms) end;
    3.10  
    3.11  in
     4.1 --- a/src/FOL/FOL.thy	Wed Apr 10 18:51:21 2013 +0200
     4.2 +++ b/src/FOL/FOL.thy	Wed Apr 10 19:14:47 2013 +0200
     4.3 @@ -181,24 +181,19 @@
     4.4  open Basic_Classical;
     4.5  *}
     4.6  
     4.7 -setup {*
     4.8 -  ML_Antiquote.value @{binding claset}
     4.9 -    (Scan.succeed "Cla.claset_of ML_context")
    4.10 -*}
    4.11 -
    4.12  setup Cla.setup
    4.13  
    4.14  (*Propositional rules*)
    4.15  lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
    4.16    and [elim!] = conjE disjE impCE FalseE iffCE
    4.17 -ML {* val prop_cs = @{claset} *}
    4.18 +ML {* val prop_cs = claset_of @{context} *}
    4.19  
    4.20  (*Quantifier rules*)
    4.21  lemmas [intro!] = allI ex_ex1I
    4.22    and [intro] = exI
    4.23    and [elim!] = exE alt_ex1E
    4.24    and [elim] = allE
    4.25 -ML {* val FOL_cs = @{claset} *}
    4.26 +ML {* val FOL_cs = claset_of @{context} *}
    4.27  
    4.28  ML {*
    4.29    structure Blast = Blast
     5.1 --- a/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Wed Apr 10 18:51:21 2013 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Wed Apr 10 19:14:47 2013 +0200
     5.3 @@ -105,7 +105,7 @@
     5.4    (rtac uexhaust THEN'
     5.5     EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex])]) cases)) 1;
     5.6  
     5.7 -val naked_ctxt = Proof_Context.init_global @{theory HOL};
     5.8 +val naked_ctxt = @{theory_context HOL};
     5.9  
    5.10  (* TODO: More precise "simp_thms"; get rid of "blast_tac" *)
    5.11  fun mk_split_tac uexhaust cases injectss distinctsss =
     6.1 --- a/src/HOL/HOL.thy	Wed Apr 10 18:51:21 2013 +0200
     6.2 +++ b/src/HOL/HOL.thy	Wed Apr 10 19:14:47 2013 +0200
     6.3 @@ -844,11 +844,6 @@
     6.4  open Basic_Classical;
     6.5  *}
     6.6  
     6.7 -setup {*
     6.8 -  ML_Antiquote.value @{binding claset}
     6.9 -    (Scan.succeed "Classical.claset_of ML_context")
    6.10 -*}
    6.11 -
    6.12  setup Classical.setup
    6.13  
    6.14  setup {*
    6.15 @@ -889,7 +884,7 @@
    6.16  declare exE [elim!]
    6.17    allE [elim]
    6.18  
    6.19 -ML {* val HOL_cs = @{claset} *}
    6.20 +ML {* val HOL_cs = claset_of @{context} *}
    6.21  
    6.22  lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
    6.23    apply (erule swap)
     7.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Wed Apr 10 18:51:21 2013 +0200
     7.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Wed Apr 10 19:14:47 2013 +0200
     7.3 @@ -400,7 +400,7 @@
     7.4        ==> input_enabled (A||B)"
     7.5  apply (unfold input_enabled_def)
     7.6  apply (simp add: Let_def inputs_of_par trans_of_par)
     7.7 -apply (tactic "safe_tac (Proof_Context.init_global @{theory Fun})")
     7.8 +apply (tactic "safe_tac @{theory_context Fun}")
     7.9  apply (simp add: inp_is_act)
    7.10  prefer 2
    7.11  apply (simp add: inp_is_act)
     8.1 --- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed Apr 10 18:51:21 2013 +0200
     8.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed Apr 10 19:14:47 2013 +0200
     8.3 @@ -298,7 +298,7 @@
     8.4    let val ss = simpset_of ctxt in
     8.5      EVERY'[Seq_induct_tac ctxt sch defs,
     8.6             asm_full_simp_tac ss,
     8.7 -           SELECT_GOAL (safe_tac (Proof_Context.init_global @{theory Fun})),
     8.8 +           SELECT_GOAL (safe_tac @{theory_context Fun}),
     8.9             Seq_case_simp_tac ctxt exA,
    8.10             Seq_case_simp_tac ctxt exB,
    8.11             asm_full_simp_tac ss,
     9.1 --- a/src/HOL/HOLCF/Tools/Domain/domain.ML	Wed Apr 10 18:51:21 2013 +0200
     9.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain.ML	Wed Apr 10 19:14:47 2013 +0200
     9.3 @@ -44,7 +44,7 @@
     9.4  fun add_arity ((b, sorts, mx), sort) thy : theory =
     9.5    thy
     9.6    |> Sign.add_types_global [(b, length sorts, mx)]
     9.7 -  |> AxClass.axiomatize_arity (Sign.full_name thy b, sorts, sort)
     9.8 +  |> Axclass.axiomatize_arity (Sign.full_name thy b, sorts, sort)
     9.9  
    9.10  fun gen_add_domain
    9.11      (prep_sort : theory -> 'a -> sort)
    10.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Wed Apr 10 18:51:21 2013 +0200
    10.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_axioms.ML	Wed Apr 10 19:14:47 2013 +0200
    10.3 @@ -104,7 +104,7 @@
    10.4      fun thy_arity (_, _, (lhsT, _)) =
    10.5          let val (dname, tvars) = dest_Type lhsT
    10.6          in (dname, map (snd o dest_TFree) tvars, @{sort pcpo}) end
    10.7 -    val thy = fold (AxClass.axiomatize_arity o thy_arity) dom_eqns thy
    10.8 +    val thy = fold (Axclass.axiomatize_arity o thy_arity) dom_eqns thy
    10.9  
   10.10      (* declare and axiomatize abs/rep *)
   10.11      val (iso_infos, thy) =
    11.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Apr 10 18:51:21 2013 +0200
    11.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Wed Apr 10 19:14:47 2013 +0200
    11.3 @@ -427,7 +427,7 @@
    11.4          fun arity (vs, tbind, _, _, _) =
    11.5            (Sign.full_name thy tbind, map the_sort vs, @{sort "domain"})
    11.6        in
    11.7 -        fold AxClass.axiomatize_arity (map arity doms) tmp_thy
    11.8 +        fold Axclass.axiomatize_arity (map arity doms) tmp_thy
    11.9        end
   11.10  
   11.11      (* check bifiniteness of right-hand sides *)
    12.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Wed Apr 10 18:51:21 2013 +0200
    12.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Wed Apr 10 19:14:47 2013 +0200
    12.3 @@ -74,7 +74,7 @@
    12.4      val (full_tname, Ts) = dest_Type newT
    12.5      val lhs_sorts = map (snd o dest_TFree) Ts
    12.6      val tac = Tactic.rtac (@{thm typedef_cpo} OF cpo_thms) 1
    12.7 -    val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy
    12.8 +    val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort cpo}) (K tac) thy
    12.9      (* transfer thms so that they will know about the new cpo instance *)
   12.10      val cpo_thms' = map (Thm.transfer thy) cpo_thms
   12.11      fun make thm = Drule.zero_var_indexes (thm OF cpo_thms')
   12.12 @@ -113,7 +113,7 @@
   12.13      val (full_tname, Ts) = dest_Type newT
   12.14      val lhs_sorts = map (snd o dest_TFree) Ts
   12.15      val tac = Tactic.rtac (@{thm typedef_pcpo} OF pcpo_thms) 1
   12.16 -    val thy = AxClass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy
   12.17 +    val thy = Axclass.prove_arity (full_tname, lhs_sorts, @{sort pcpo}) (K tac) thy
   12.18      val pcpo_thms' = map (Thm.transfer thy) pcpo_thms
   12.19      fun make thm = Drule.zero_var_indexes (thm OF pcpo_thms')
   12.20      val Rep_strict = make @{thm typedef_Rep_strict}
    13.1 --- a/src/HOL/Library/refute.ML	Wed Apr 10 18:51:21 2013 +0200
    13.2 +++ b/src/HOL/Library/refute.ML	Wed Apr 10 19:14:47 2013 +0200
    13.3 @@ -695,7 +695,7 @@
    13.4          val superclasses = distinct (op =) superclasses
    13.5          val class_axioms = maps (fn class => map (fn ax =>
    13.6            ("<" ^ class ^ ">", Thm.prop_of ax))
    13.7 -          (#axioms (AxClass.get_info thy class) handle ERROR _ => []))
    13.8 +          (#axioms (Axclass.get_info thy class) handle ERROR _ => []))
    13.9            superclasses
   13.10          (* replace the (at most one) schematic type variable in each axiom *)
   13.11          (* by the actual type 'T'                                          *)
    14.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Apr 10 18:51:21 2013 +0200
    14.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Wed Apr 10 19:14:47 2013 +0200
    14.3 @@ -200,7 +200,7 @@
    14.4  apply( simp_all)
    14.5  apply( tactic "ALLGOALS (REPEAT o resolve_tac [impI, allI])")
    14.6  apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
    14.7 -                 THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *})
    14.8 +                 THEN_ALL_NEW (full_simp_tac (simpset_of @{theory_context Conform}))) *})
    14.9  apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
   14.10  
   14.11  -- "Level 7"
    15.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Wed Apr 10 18:51:21 2013 +0200
    15.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Wed Apr 10 19:14:47 2013 +0200
    15.3 @@ -311,7 +311,7 @@
    15.4                         (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
    15.5                          HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
    15.6        in
    15.7 -          AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
    15.8 +          Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
    15.9                  [((Binding.name (cl_name ^ "1"), [Simplifier.simp_add]), [axiom1]),
   15.10                   ((Binding.name (cl_name ^ "2"), []), [axiom2]),                           
   15.11                   ((Binding.name (cl_name ^ "3"), []), [axiom3])] thy
   15.12 @@ -360,7 +360,7 @@
   15.13            val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
   15.14  
   15.15         in  
   15.16 -        AxClass.define_class (Binding.name cl_name, [pt_name]) []
   15.17 +        Axclass.define_class (Binding.name cl_name, [pt_name]) []
   15.18            [((Binding.name (cl_name ^ "1"), []), [axiom1])] thy
   15.19         end) ak_names_types thy8; 
   15.20           
   15.21 @@ -410,7 +410,7 @@
   15.22                             (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
   15.23                                             cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
   15.24                 in  
   15.25 -                 AxClass.define_class (Binding.name cl_name, ["HOL.type"]) []
   15.26 +                 Axclass.define_class (Binding.name cl_name, ["HOL.type"]) []
   15.27                     [((Binding.name (cl_name ^ "1"), []), [ax1])] thy'  
   15.28                 end) ak_names_types thy) ak_names_types thy12;
   15.29  
   15.30 @@ -517,7 +517,7 @@
   15.31  
   15.32           in
   15.33             thy'
   15.34 -           |> AxClass.prove_arity (qu_name,[],[cls_name])
   15.35 +           |> Axclass.prove_arity (qu_name,[],[cls_name])
   15.36                (fn _ => if ak_name = ak_name' then proof1 else proof2)
   15.37           end) ak_names thy) ak_names thy12d;
   15.38  
   15.39 @@ -551,15 +551,15 @@
   15.40            val pt_thm_unit  = pt_unit_inst;
   15.41         in
   15.42          thy
   15.43 -        |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
   15.44 -        |> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
   15.45 -        |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
   15.46 -        |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
   15.47 -        |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
   15.48 -        |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
   15.49 -        |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   15.50 +        |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_fun)
   15.51 +        |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (pt_proof pt_thm_set)
   15.52 +        |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
   15.53 +        |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
   15.54 +        |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
   15.55 +        |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
   15.56 +        |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   15.57                                      (pt_proof pt_thm_nprod)
   15.58 -        |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
   15.59 +        |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
   15.60       end) ak_names thy13; 
   15.61  
   15.62         (********  fs_<ak> class instances  ********)
   15.63 @@ -592,7 +592,7 @@
   15.64                        val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI];
   15.65                    in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end)
   15.66          in
   15.67 -         AxClass.prove_arity (qu_name,[],[qu_class]) (fn _ => proof) thy'
   15.68 +         Axclass.prove_arity (qu_name,[],[qu_class]) (fn _ => proof) thy'
   15.69          end) ak_names thy) ak_names thy18;
   15.70  
   15.71         (* shows that                  *)
   15.72 @@ -616,12 +616,12 @@
   15.73            val fs_thm_optn  = fs_inst RS fs_option_inst;
   15.74          in 
   15.75           thy
   15.76 -         |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
   15.77 -         |> AxClass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
   15.78 -         |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   15.79 +         |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
   15.80 +         |> Axclass.prove_arity (@{type_name Product_Type.prod},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
   15.81 +         |> Axclass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
   15.82                                       (fs_proof fs_thm_nprod) 
   15.83 -         |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
   15.84 -         |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
   15.85 +         |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
   15.86 +         |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (fs_proof fs_thm_optn)
   15.87          end) ak_names thy20;
   15.88  
   15.89         (********  cp_<ak>_<ai> class instances  ********)
   15.90 @@ -669,7 +669,7 @@
   15.91                      EVERY [Class.intro_classes_tac [], simp_tac simp_s 1]
   15.92                    end))
   15.93                in
   15.94 -                AxClass.prove_arity (name,[],[cls_name]) (fn _ => proof) thy''
   15.95 +                Axclass.prove_arity (name,[],[cls_name]) (fn _ => proof) thy''
   15.96                end) ak_names thy') ak_names thy) ak_names thy24;
   15.97  
   15.98         (* shows that                                                    *) 
   15.99 @@ -700,13 +700,13 @@
  15.100              val cp_thm_set = cp_inst RS cp_set_inst;
  15.101          in
  15.102           thy'
  15.103 -         |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
  15.104 -         |> AxClass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
  15.105 -         |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
  15.106 -         |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
  15.107 -         |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
  15.108 -         |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
  15.109 -         |> AxClass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
  15.110 +         |> Axclass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
  15.111 +         |> Axclass.prove_arity (@{type_name Product_Type.prod}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
  15.112 +         |> Axclass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
  15.113 +         |> Axclass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
  15.114 +         |> Axclass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
  15.115 +         |> Axclass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (cp_proof cp_thm_noptn)
  15.116 +         |> Axclass.prove_arity (@{type_name Set.set},[[cls_name]],[cls_name]) (cp_proof cp_thm_set)
  15.117          end) ak_names thy) ak_names thy25;
  15.118  
  15.119       (* show that discrete nominal types are permutation types, finitely     *)
  15.120 @@ -722,7 +722,7 @@
  15.121                 val simp_s = HOL_basic_ss addsimps [Simpdata.mk_eq defn];
  15.122                 val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
  15.123               in 
  15.124 -               AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
  15.125 +               Axclass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
  15.126               end) ak_names;
  15.127  
  15.128            fun discrete_fs_inst discrete_ty defn = 
  15.129 @@ -733,7 +733,7 @@
  15.130                 val simp_s = HOL_ss addsimps [supp_def, Collect_const, finite_emptyI, Simpdata.mk_eq defn];
  15.131                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
  15.132               in 
  15.133 -               AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
  15.134 +               Axclass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
  15.135               end) ak_names;
  15.136  
  15.137            fun discrete_cp_inst discrete_ty defn = 
  15.138 @@ -744,7 +744,7 @@
  15.139                 val simp_s = HOL_ss addsimps [Simpdata.mk_eq defn];
  15.140                 val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
  15.141               in
  15.142 -               AxClass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
  15.143 +               Axclass.prove_arity (discrete_ty, [], [qu_class]) (fn _ => proof) thy
  15.144               end) ak_names)) ak_names;
  15.145  
  15.146          in
    16.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Apr 10 18:51:21 2013 +0200
    16.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Apr 10 19:14:47 2013 +0200
    16.3 @@ -425,7 +425,7 @@
    16.4            (fn {context = ctxt, ...} => EVERY [Datatype_Aux.ind_tac induct perm_indnames 1,
    16.5               ALLGOALS (asm_full_simp_tac (simps ctxt))]))
    16.6        in
    16.7 -        fold (fn (s, tvs) => fn thy => AxClass.prove_arity
    16.8 +        fold (fn (s, tvs) => fn thy => Axclass.prove_arity
    16.9              (s, map (inter_sort thy sort o snd) tvs, [cp_class])
   16.10              (fn _ => Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
   16.11            (full_new_type_names' ~~ tyvars) thy
   16.12 @@ -437,7 +437,7 @@
   16.13        fold (fn atom => fn thy =>
   16.14          let val pt_name = pt_class_of thy atom
   16.15          in
   16.16 -          fold (fn (s, tvs) => fn thy => AxClass.prove_arity
   16.17 +          fold (fn (s, tvs) => fn thy => Axclass.prove_arity
   16.18                (s, map (inter_sort thy [pt_name] o snd) tvs, [pt_name])
   16.19                (fn _ => EVERY
   16.20                  [Class.intro_classes_tac [],
   16.21 @@ -618,7 +618,7 @@
   16.22              val pt_class = pt_class_of thy atom;
   16.23              val sort = Sign.minimize_sort thy (Sign.certify_sort thy
   16.24                (pt_class :: map (cp_class_of thy atom) (remove (op =) atom dt_atoms)))
   16.25 -          in AxClass.prove_arity
   16.26 +          in Axclass.prove_arity
   16.27              (Sign.intern_type thy name,
   16.28                map (inter_sort thy sort o snd) tvs, [pt_class])
   16.29              (fn ctxt => EVERY [Class.intro_classes_tac [],
   16.30 @@ -648,7 +648,7 @@
   16.31          val cp1' = cp_inst_of thy atom1 atom2 RS cp1
   16.32        in fold (fn ((((((Abs_inverse, Rep),
   16.33          perm_def), name), tvs), perm_closed1), perm_closed2) => fn thy =>
   16.34 -          AxClass.prove_arity
   16.35 +          Axclass.prove_arity
   16.36              (Sign.intern_type thy name,
   16.37                map (inter_sort thy sort o snd) tvs, [cp_class])
   16.38              (fn ctxt => EVERY [Class.intro_classes_tac [],
   16.39 @@ -1105,7 +1105,7 @@
   16.40          let
   16.41            val class = fs_class_of thy atom;
   16.42            val sort = Sign.minimize_sort thy (Sign.certify_sort thy (class :: pt_cp_sort));
   16.43 -        in fold (fn Type (s, Ts) => AxClass.prove_arity
   16.44 +        in fold (fn Type (s, Ts) => Axclass.prove_arity
   16.45            (s, map (inter_sort thy sort o snd o dest_TFree) Ts, [class])
   16.46            (fn _ => Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
   16.47          end) (atoms ~~ finite_supp_thms) ||>
    17.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Apr 10 18:51:21 2013 +0200
    17.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Apr 10 19:14:47 2013 +0200
    17.3 @@ -19,7 +19,7 @@
    17.4  fun mk_constr_consts thy vs tyco cos =
    17.5    let
    17.6      val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos;
    17.7 -    val cs' = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) cs;
    17.8 +    val cs' = map (fn c_ty as (_, ty) => (Axclass.unoverload_const thy c_ty, ty)) cs;
    17.9    in
   17.10      if is_some (try (Code.constrset_of_consts thy) cs')
   17.11      then SOME cs
   17.12 @@ -54,7 +54,7 @@
   17.13      |> Raw_Simplifier.rewrite_rule [Thm.symmetric (Thm.assume asm)]
   17.14      |> Thm.implies_intr asm
   17.15      |> Thm.generalize ([], params) 0
   17.16 -    |> AxClass.unoverload thy
   17.17 +    |> Axclass.unoverload thy
   17.18      |> Thm.varifyT_global
   17.19    end;
   17.20  
    18.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Apr 10 18:51:21 2013 +0200
    18.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Apr 10 19:14:47 2013 +0200
    18.3 @@ -1028,7 +1028,7 @@
    18.4        let
    18.5          val supers = Sign.complete_sort thy S
    18.6          val class_axioms =
    18.7 -          maps (fn class => map prop_of (AxClass.get_info thy class |> #axioms
    18.8 +          maps (fn class => map prop_of (Axclass.get_info thy class |> #axioms
    18.9                                           handle ERROR _ => [])) supers
   18.10          val monomorphic_class_axioms =
   18.11            map (fn t => case Term.add_tvars t [] of
    19.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Apr 10 18:51:21 2013 +0200
    19.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Wed Apr 10 19:14:47 2013 +0200
    19.3 @@ -36,7 +36,7 @@
    19.4        ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
    19.5      |> space_implode "\n" |> tracing
    19.6    else ()
    19.7 -fun overload_const thy s = the_default s (Option.map fst (AxClass.inst_of_param thy s))
    19.8 +fun overload_const thy s = the_default s (Option.map fst (Axclass.inst_of_param thy s))
    19.9  
   19.10  fun map_specs f specs =
   19.11    map (fn (s, ths) => (s, f ths)) specs
   19.12 @@ -109,7 +109,7 @@
   19.13        val intross5 = map_specs (map (remove_equalities thy2)) intross4
   19.14        val _ = print_intross options thy2 "After removing equality premises:" intross5
   19.15        val intross6 =
   19.16 -        map (fn (s, ths) => (overload_const thy2 s, map (AxClass.overload thy2) ths)) intross5
   19.17 +        map (fn (s, ths) => (overload_const thy2 s, map (Axclass.overload thy2) ths)) intross5
   19.18        val intross7 = map_specs (map (expand_tuples thy2)) intross6
   19.19        val intross8 = map_specs (map (eta_contract_ho_arguments thy2)) intross7
   19.20        val _ = case !intro_hook of NONE => () | SOME f => (map_specs (map (f thy2)) intross8; ())
    20.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Apr 10 18:51:21 2013 +0200
    20.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Apr 10 19:14:47 2013 +0200
    20.3 @@ -189,7 +189,7 @@
    20.4  fun get_specification options thy t =
    20.5    let
    20.6      (*val (c, T) = dest_Const t
    20.7 -    val t = Const (AxClass.unoverload_const thy (c, T), T)*)
    20.8 +    val t = Const (Axclass.unoverload_const thy (c, T), T)*)
    20.9      val _ = if show_steps options then
   20.10          tracing ("getting specification of " ^ Syntax.string_of_term_global thy t ^
   20.11            " with type " ^ Syntax.string_of_typ_global thy (fastype_of t))
    21.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 10 18:51:21 2013 +0200
    21.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Wed Apr 10 19:14:47 2013 +0200
    21.3 @@ -93,7 +93,7 @@
    21.4      val ty = Type (tyco, map TFree vs);
    21.5      val cs = (map o apsnd o apsnd o map o map_atyps)
    21.6        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    21.7 -    val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
    21.8 +    val const = Axclass.param_of_inst thy (@{const_name partial_term_of}, tyco);
    21.9      val var_insts =
   21.10        map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
   21.11          [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Narrowing_variable p tt"},
    22.1 --- a/src/HOL/Tools/code_evaluation.ML	Wed Apr 10 18:51:21 2013 +0200
    22.2 +++ b/src/HOL/Tools/code_evaluation.ML	Wed Apr 10 19:14:47 2013 +0200
    22.3 @@ -78,7 +78,7 @@
    22.4      val ty = Type (tyco, map TFree vs);
    22.5      val cs = (map o apsnd o apsnd o map o map_atyps)
    22.6        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    22.7 -    val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
    22.8 +    val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco);
    22.9      val eqs = map (mk_term_of_eq thy ty) cs;
   22.10   in
   22.11      thy
   22.12 @@ -115,7 +115,7 @@
   22.13      val ty = Type (tyco, map TFree vs);
   22.14      val ty_rep = map_atyps
   22.15        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep;
   22.16 -    val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco);
   22.17 +    val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco);
   22.18      val eq = mk_abs_term_of_eq thy ty abs ty_rep proj;
   22.19   in
   22.20      thy
   22.21 @@ -169,7 +169,7 @@
   22.22  
   22.23  fun mk_term_of t = HOLogic.mk_term_of (fastype_of t) t;
   22.24  
   22.25 -fun term_of_const_for thy = AxClass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
   22.26 +fun term_of_const_for thy = Axclass.unoverload_const thy o dest_Const o HOLogic.term_of_const;
   22.27  
   22.28  fun gen_dynamic_value dynamic_value thy t =
   22.29    dynamic_value cookie thy NONE I (mk_term_of t) [];
   22.30 @@ -204,7 +204,7 @@
   22.31  fun static_conv thy consts Ts =
   22.32    let
   22.33      val eqs = "==" :: @{const_name HOL.eq} ::
   22.34 -      map (fn T => AxClass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
   22.35 +      map (fn T => Axclass.unoverload_const thy (@{const_name HOL.equal}, T)) Ts;
   22.36          (*assumes particular code equations for "==" etc.*)
   22.37    in
   22.38      certify_eval thy (static_value thy consts Ts)
    23.1 --- a/src/HOL/Tools/record.ML	Wed Apr 10 18:51:21 2013 +0200
    23.2 +++ b/src/HOL/Tools/record.ML	Wed Apr 10 19:14:47 2013 +0200
    23.3 @@ -1746,12 +1746,12 @@
    23.4          THEN ALLGOALS (rtac @{thm refl});
    23.5        fun mk_eq thy eq_def =
    23.6          Simplifier.rewrite_rule
    23.7 -          [AxClass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
    23.8 +          [Axclass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
    23.9        fun mk_eq_refl thy =
   23.10          @{thm equal_refl}
   23.11          |> Thm.instantiate
   23.12            ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
   23.13 -        |> AxClass.unoverload thy;
   23.14 +        |> Axclass.unoverload thy;
   23.15        val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
   23.16        val ensure_exhaustive_record =
   23.17          ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
    24.1 --- a/src/HOL/Word/WordBitwise.thy	Wed Apr 10 18:51:21 2013 +0200
    24.2 +++ b/src/HOL/Word/WordBitwise.thy	Wed Apr 10 19:14:47 2013 +0200
    24.3 @@ -501,7 +501,7 @@
    24.4  
    24.5  structure Word_Bitwise_Tac = struct
    24.6  
    24.7 -val word_ss = global_simpset_of @{theory Word};
    24.8 +val word_ss = simpset_of @{theory_context Word};
    24.9  
   24.10  fun mk_nat_clist ns = List.foldr
   24.11    (uncurry (Thm.mk_binop @{cterm "Cons :: nat => _"}))
    25.1 --- a/src/Provers/classical.ML	Wed Apr 10 18:51:21 2013 +0200
    25.2 +++ b/src/Provers/classical.ML	Wed Apr 10 19:14:47 2013 +0200
    25.3 @@ -56,7 +56,6 @@
    25.4    val appSWrappers: Proof.context -> wrapper
    25.5    val appWrappers: Proof.context -> wrapper
    25.6  
    25.7 -  val global_claset_of: theory -> claset
    25.8    val claset_of: Proof.context -> claset
    25.9    val map_claset: (claset -> claset) -> Proof.context -> Proof.context
   25.10    val put_claset: claset -> Proof.context -> Proof.context
   25.11 @@ -596,7 +595,6 @@
   25.12    val merge = merge_cs;
   25.13  );
   25.14  
   25.15 -val global_claset_of = Claset.get o Context.Theory;
   25.16  val claset_of = Claset.get o Context.Proof;
   25.17  val rep_claset_of = rep_cs o claset_of;
   25.18  
    26.1 --- a/src/Pure/Isar/class.ML	Wed Apr 10 18:51:21 2013 +0200
    26.2 +++ b/src/Pure/Isar/class.ML	Wed Apr 10 19:14:47 2013 +0200
    26.3 @@ -127,7 +127,7 @@
    26.4    let
    26.5      fun params class =
    26.6        let
    26.7 -        val const_typs = (#params o AxClass.get_info thy) class;
    26.8 +        val const_typs = (#params o Axclass.get_info thy) class;
    26.9          val const_names = (#consts o the_class_data thy) class;
   26.10        in
   26.11          (map o apsnd)
   26.12 @@ -190,7 +190,7 @@
   26.13          ([Pretty.command "class", Pretty.brk 1,
   26.14            Pretty.mark_str (Name_Space.markup_extern ctxt class_space class), Pretty.str ":",
   26.15            Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
   26.16 -          (case try (AxClass.get_info thy) class of
   26.17 +          (case try (Axclass.get_info thy) class of
   26.18              NONE => []
   26.19            | SOME {params, ...} =>
   26.20                [Pretty.fbrk, Pretty.big_list "parameters:" (map prt_param params)]) @
   26.21 @@ -263,7 +263,7 @@
   26.22        | NONE => I);
   26.23    in
   26.24      thy
   26.25 -    |> AxClass.add_classrel classrel
   26.26 +    |> Axclass.add_classrel classrel
   26.27      |> Class_Data.map (Graph.add_edge (sub, sup))
   26.28      |> activate_defs sub (these_defs thy diff_sort)
   26.29      |> add_dependency
   26.30 @@ -401,7 +401,7 @@
   26.31  fun gen_classrel mk_prop classrel thy =
   26.32    let
   26.33      fun after_qed results =
   26.34 -      Proof_Context.background_theory ((fold o fold) AxClass.add_classrel results);
   26.35 +      Proof_Context.background_theory ((fold o fold) Axclass.add_classrel results);
   26.36    in
   26.37      thy
   26.38      |> Proof_Context.init_global
   26.39 @@ -411,9 +411,9 @@
   26.40  in
   26.41  
   26.42  val classrel =
   26.43 -  gen_classrel (Logic.mk_classrel oo AxClass.cert_classrel);
   26.44 +  gen_classrel (Logic.mk_classrel oo Axclass.cert_classrel);
   26.45  val classrel_cmd =
   26.46 -  gen_classrel (Logic.mk_classrel oo AxClass.read_classrel);
   26.47 +  gen_classrel (Logic.mk_classrel oo Axclass.read_classrel);
   26.48  
   26.49  end; (*local*)
   26.50  
   26.51 @@ -472,7 +472,7 @@
   26.52    let
   26.53      val Instantiation {params, ...} = Instantiation.get ctxt;
   26.54  
   26.55 -    val lookup_inst_param = AxClass.lookup_inst_param
   26.56 +    val lookup_inst_param = Axclass.lookup_inst_param
   26.57        (Sign.consts_of (Proof_Context.theory_of ctxt)) params;
   26.58      fun subst (c, ty) =
   26.59        (case lookup_inst_param (c, ty) of
   26.60 @@ -505,8 +505,8 @@
   26.61  (* target *)
   26.62  
   26.63  fun define_overloaded (c, U) v (b_def, rhs) =
   26.64 -  Local_Theory.background_theory_result (AxClass.declare_overloaded (c, U)
   26.65 -  ##>> AxClass.define_overloaded b_def (c, rhs))
   26.66 +  Local_Theory.background_theory_result (Axclass.declare_overloaded (c, U)
   26.67 +  ##>> Axclass.define_overloaded b_def (c, rhs))
   26.68    ##> (map_instantiation o apsnd) (filter_out (fn (_, (v', _)) => v' = v))
   26.69    ##> Local_Theory.map_contexts (K synchronize_inst_syntax);
   26.70  
   26.71 @@ -541,9 +541,9 @@
   26.72      val naming = Sign.naming_of thy;
   26.73  
   26.74      val _ = if null tycos then error "At least one arity must be given" else ();
   26.75 -    val class_params = these_params thy (filter (can (AxClass.get_info thy)) sort);
   26.76 +    val class_params = these_params thy (filter (can (Axclass.get_info thy)) sort);
   26.77      fun get_param tyco (param, (_, (c, ty))) =
   26.78 -      if can (AxClass.param_of_inst thy) (c, tyco)
   26.79 +      if can (Axclass.param_of_inst thy) (c, tyco)
   26.80        then NONE else SOME ((c, tyco),
   26.81          (param ^ "_" ^ Long_Name.base_name tyco, map_atyps (K (Type (tyco, map TFree vs))) ty));
   26.82      val params = map_product get_param tycos class_params |> map_filter I;
   26.83 @@ -559,7 +559,7 @@
   26.84      val improve_constraints = AList.lookup (op =)
   26.85        (map (fn (_, (class, (c, _))) => (c, [[class]])) class_params);
   26.86      fun resort_check ctxt ts = resort_terms ctxt algebra consts improve_constraints ts;
   26.87 -    val lookup_inst_param = AxClass.lookup_inst_param consts params;
   26.88 +    val lookup_inst_param = Axclass.lookup_inst_param consts params;
   26.89      fun improve (c, ty) =
   26.90        (case lookup_inst_param (c, ty) of
   26.91          SOME (_, ty') => if Sign.typ_instance thy (ty', ty) then SOME (ty, ty') else NONE
   26.92 @@ -593,7 +593,7 @@
   26.93      val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
   26.94      val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
   26.95      fun after_qed' results =
   26.96 -      Local_Theory.background_theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
   26.97 +      Local_Theory.background_theory (fold (Axclass.add_arity o Thm.varifyT_global) results)
   26.98        #> after_qed;
   26.99    in
  26.100      lthy
  26.101 @@ -630,7 +630,7 @@
  26.102      val sorts = map snd vs;
  26.103      val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
  26.104      fun after_qed results =
  26.105 -      Proof_Context.background_theory ((fold o fold) AxClass.add_arity results);
  26.106 +      Proof_Context.background_theory ((fold o fold) Axclass.add_arity results);
  26.107    in
  26.108      thy
  26.109      |> Proof_Context.init_global
  26.110 @@ -645,7 +645,7 @@
  26.111      val thy = Thm.theory_of_thm st;
  26.112      val classes = Sign.all_classes thy;
  26.113      val class_trivs = map (Thm.class_triv thy) classes;
  26.114 -    val class_intros = map_filter (try (#intro o AxClass.get_info thy)) classes;
  26.115 +    val class_intros = map_filter (try (#intro o Axclass.get_info thy)) classes;
  26.116      val assm_intros = all_assm_intros thy;
  26.117    in
  26.118      Method.intros_tac (class_trivs @ class_intros @ assm_intros) facts st
    27.1 --- a/src/Pure/Isar/class_declaration.ML	Wed Apr 10 18:51:21 2013 +0200
    27.2 +++ b/src/Pure/Isar/class_declaration.ML	Wed Apr 10 19:14:47 2013 +0200
    27.3 @@ -90,7 +90,7 @@
    27.4            ((map_types o map_atyps) (K aT) prop), of_class_prop_concl));
    27.5      val sup_of_classes = map (snd o Class.rules thy) sups;
    27.6      val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
    27.7 -    val axclass_intro = #intro (AxClass.get_info thy class);
    27.8 +    val axclass_intro = #intro (Axclass.get_info thy class);
    27.9      val base_sort_trivs = Thm.of_sort (Thm.ctyp_of thy aT, base_sort);
   27.10      val tac =
   27.11        REPEAT (SOMEGOAL
   27.12 @@ -289,13 +289,13 @@
   27.13        |> fst
   27.14        |> Option.map (Logic.unvarify_global o Logic.strip_imp_concl o Thm.prop_of);
   27.15      fun get_axiom thy =
   27.16 -      (case #axioms (AxClass.get_info thy class) of
   27.17 +      (case #axioms (Axclass.get_info thy class) of
   27.18           [] => NONE
   27.19        | [thm] => SOME thm);
   27.20    in
   27.21      thy
   27.22      |> add_consts class base_sort sups supparam_names global_syntax
   27.23 -    |-> (fn (param_map, params) => AxClass.define_class (bname, supsort)
   27.24 +    |-> (fn (param_map, params) => Axclass.define_class (bname, supsort)
   27.25            (map (fst o snd) params)
   27.26            [(Thm.empty_binding, Option.map (globalize param_map) raw_pred |> the_list)]
   27.27      #> snd
   27.28 @@ -346,7 +346,7 @@
   27.29        (case Named_Target.peek lthy of
   27.30           SOME {target, is_class = true, ...} => target
   27.31        | _ => error "Not in a class target");
   27.32 -    val (sub, sup) = AxClass.cert_classrel thy (proto_sub, proto_sup);
   27.33 +    val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup);
   27.34  
   27.35      val expr = ([(sup, (("", false), Expression.Positional []))], []);
   27.36      val (([props], deps, export), goal_ctxt) =
    28.1 --- a/src/Pure/Isar/code.ML	Wed Apr 10 18:51:21 2013 +0200
    28.2 +++ b/src/Pure/Isar/code.ML	Wed Apr 10 19:14:47 2013 +0200
    28.3 @@ -107,7 +107,7 @@
    28.4  
    28.5  fun string_of_const thy c =
    28.6    let val ctxt = Proof_Context.init_global thy in
    28.7 -    case AxClass.inst_of_param thy c of
    28.8 +    case Axclass.inst_of_param thy c of
    28.9        SOME (c, tyco) =>
   28.10          Proof_Context.extern_const ctxt c ^ " " ^ enclose "[" "]"
   28.11            (Proof_Context.extern_type ctxt tyco)
   28.12 @@ -140,7 +140,7 @@
   28.13  
   28.14  fun check_unoverload thy (c, ty) =
   28.15    let
   28.16 -    val c' = AxClass.unoverload_const thy (c, ty);
   28.17 +    val c' = Axclass.unoverload_const thy (c, ty);
   28.18      val ty_decl = Sign.the_const_type thy c';
   28.19    in
   28.20      if typscheme_equiv (ty_decl, Logic.varifyT_global ty)
   28.21 @@ -375,7 +375,7 @@
   28.22  
   28.23  fun constrset_of_consts thy consts =
   28.24    let
   28.25 -    val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c
   28.26 +    val _ = map (fn (c, _) => if (is_some o Axclass.class_of_param thy) c
   28.27        then error ("Is a class parameter: " ^ string_of_const thy c) else ()) consts;
   28.28      val raw_constructors = map (analyze_constructor thy) consts;
   28.29      val tyco = case distinct (op =) (map (fst o fst) raw_constructors)
   28.30 @@ -477,7 +477,7 @@
   28.31        else bad_thm "Free type variables on right hand side of equation";
   28.32      val (head, args) = strip_comb lhs;
   28.33      val (c, ty) = case head
   28.34 -     of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty)
   28.35 +     of Const (c_ty as (_, ty)) => (Axclass.unoverload_const thy c_ty, ty)
   28.36        | _ => bad_thm "Equation not headed by constant";
   28.37      fun check _ (Abs _) = bad_thm "Abstraction on left hand side of equation"
   28.38        | check 0 (Var _) = ()
   28.39 @@ -485,7 +485,7 @@
   28.40        | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
   28.41        | check n (Const (c_ty as (c, ty))) =
   28.42            if allow_pats then let
   28.43 -            val c' = AxClass.unoverload_const thy c_ty
   28.44 +            val c' = Axclass.unoverload_const thy c_ty
   28.45            in if n = (length o binder_types) ty
   28.46              then if allow_consts orelse is_constr thy c'
   28.47                then ()
   28.48 @@ -495,7 +495,7 @@
   28.49      val _ = map (check 0) args;
   28.50      val _ = if allow_nonlinear orelse is_linear thm then ()
   28.51        else bad_thm "Duplicate variables on left hand side of equation";
   28.52 -    val _ = if (is_none o AxClass.class_of_param thy) c then ()
   28.53 +    val _ = if (is_none o Axclass.class_of_param thy) c then ()
   28.54        else bad_thm "Overloaded constant as head in equation";
   28.55      val _ = if not (is_constr thy c) then ()
   28.56        else bad_thm "Constructor as head in equation";
   28.57 @@ -557,13 +557,13 @@
   28.58  fun const_typ_eqn thy thm =
   28.59    let
   28.60      val (c, ty) = head_eqn thm;
   28.61 -    val c' = AxClass.unoverload_const thy (c, ty);
   28.62 +    val c' = Axclass.unoverload_const thy (c, ty);
   28.63        (*permissive wrt. to overloaded constants!*)
   28.64    in (c', ty) end;
   28.65  
   28.66  fun const_eqn thy = fst o const_typ_eqn thy;
   28.67  
   28.68 -fun const_abs_eqn thy = AxClass.unoverload_const thy o dest_Const o fst o strip_comb o snd
   28.69 +fun const_abs_eqn thy = Axclass.unoverload_const thy o dest_Const o fst o strip_comb o snd
   28.70    o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
   28.71  
   28.72  fun mk_proj tyco vs ty abs rep =
   28.73 @@ -629,14 +629,14 @@
   28.74  
   28.75  fun check_abstype_cert thy proto_thm =
   28.76    let
   28.77 -    val thm = (AxClass.unoverload thy o meta_rewrite thy) proto_thm;
   28.78 +    val thm = (Axclass.unoverload thy o meta_rewrite thy) proto_thm;
   28.79      val (lhs, rhs) = Logic.dest_equals (Thm.plain_prop_of thm)
   28.80        handle TERM _ => bad_thm "Not an equation"
   28.81             | THM _ => bad_thm "Not a proper equation";
   28.82      val ((abs, raw_ty), ((rep, rep_ty), param)) = (apsnd (apfst dest_Const o dest_comb)
   28.83          o apfst dest_Const o dest_comb) lhs
   28.84        handle TERM _ => bad_thm "Not an abstype certificate";
   28.85 -    val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
   28.86 +    val _ = pairself (fn c => if (is_some o Axclass.class_of_param thy) c
   28.87        then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (abs, rep);
   28.88      val _ = check_decl_ty thy (abs, raw_ty);
   28.89      val _ = check_decl_ty thy (rep, rep_ty);
   28.90 @@ -714,7 +714,7 @@
   28.91    let
   28.92      val raw_ty = Logic.unvarifyT_global (const_typ thy c);
   28.93      val (vs, _) = typscheme thy (c, raw_ty);
   28.94 -    val sortargs = case AxClass.class_of_param thy c
   28.95 +    val sortargs = case Axclass.class_of_param thy c
   28.96       of SOME class => [[class]]
   28.97        | NONE => (case get_type_of_constr_or_abstr thy c
   28.98           of SOME (tyco, _) => (map snd o fst o the)
   28.99 @@ -840,12 +840,12 @@
  28.100        end;
  28.101  
  28.102  fun pretty_cert thy (cert as Equations _) =
  28.103 -      (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd)
  28.104 +      (map_filter (Option.map (Display.pretty_thm_global thy o Axclass.overload thy) o fst o snd)
  28.105           o snd o equations_of_cert thy) cert
  28.106    | pretty_cert thy (Projection (t, _)) =
  28.107        [Syntax.pretty_term_global thy (Logic.varify_types_global t)]
  28.108    | pretty_cert thy (Abstract (abs_thm, _)) =
  28.109 -      [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT_global) abs_thm];
  28.110 +      [(Display.pretty_thm_global thy o Axclass.overload thy o Thm.varifyT_global) abs_thm];
  28.111  
  28.112  fun bare_thms_of_cert thy (cert as Equations _) =
  28.113        (map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
  28.114 @@ -881,7 +881,7 @@
  28.115    (map o apfst) (Thm.transfer thy)
  28.116    #> perhaps (perhaps_loop (perhaps_apply functrans))
  28.117    #> (map o apfst) (rewrite_eqn thy eqn_conv ss) 
  28.118 -  #> (map o apfst) (AxClass.unoverload thy)
  28.119 +  #> (map o apfst) (Axclass.unoverload thy)
  28.120    #> cert_of_eqns thy c;
  28.121  
  28.122  fun get_cert thy { functrans, ss } c =
  28.123 @@ -895,7 +895,7 @@
  28.124      | Abstr (abs_thm, tyco) => abs_thm
  28.125          |> Thm.transfer thy
  28.126          |> rewrite_eqn thy Conv.arg_conv ss
  28.127 -        |> AxClass.unoverload thy
  28.128 +        |> Axclass.unoverload thy
  28.129          |> cert_of_abs thy tyco c;
  28.130  
  28.131  
  28.132 @@ -1172,7 +1172,7 @@
  28.133          #> (map_cases o apfst) drop_outdated_cases)
  28.134    end;
  28.135  
  28.136 -fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty);
  28.137 +fun unoverload_const_typ thy (c, ty) = (Axclass.unoverload_const thy (c, ty), ty);
  28.138  
  28.139  structure Datatype_Interpretation =
  28.140    Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
    29.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Apr 10 18:51:21 2013 +0200
    29.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Apr 10 19:14:47 2013 +0200
    29.3 @@ -79,13 +79,13 @@
    29.4    Outer_Syntax.command @{command_spec "classes"} "declare type classes"
    29.5      (Scan.repeat1 (Parse.binding -- Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<"}) |--
    29.6          Parse.!!! (Parse.list1 Parse.class)) [])
    29.7 -      >> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
    29.8 +      >> (Toplevel.theory o fold Axclass.axiomatize_class_cmd));
    29.9  
   29.10  val _ =
   29.11    Outer_Syntax.command @{command_spec "classrel"} "state inclusion of type classes (axiomatic!)"
   29.12      (Parse.and_list1 (Parse.class -- ((@{keyword "\<subseteq>"} || @{keyword "<"})
   29.13          |-- Parse.!!! Parse.class))
   29.14 -    >> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
   29.15 +    >> (Toplevel.theory o Axclass.axiomatize_classrel_cmd));
   29.16  
   29.17  val _ =
   29.18    Outer_Syntax.local_theory @{command_spec "default_sort"}
   29.19 @@ -113,7 +113,7 @@
   29.20  
   29.21  val _ =
   29.22    Outer_Syntax.command @{command_spec "arities"} "state type arities (axiomatic!)"
   29.23 -    (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
   29.24 +    (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold Axclass.axiomatize_arity_cmd));
   29.25  
   29.26  
   29.27  (* consts and syntax *)
    30.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 10 18:51:21 2013 +0200
    30.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 10 19:14:47 2013 +0200
    30.3 @@ -10,6 +10,7 @@
    30.4  sig
    30.5    val theory_of: Proof.context -> theory
    30.6    val init_global: theory -> Proof.context
    30.7 +  val get_global: theory -> string -> Proof.context
    30.8    type mode
    30.9    val mode_default: mode
   30.10    val mode_stmt: mode
   30.11 @@ -166,6 +167,7 @@
   30.12  
   30.13  val theory_of = Proof_Context.theory_of;
   30.14  val init_global = Proof_Context.init_global;
   30.15 +val get_global = Proof_Context.get_global;
   30.16  
   30.17  
   30.18  
    31.1 --- a/src/Pure/Isar/typedecl.ML	Wed Apr 10 18:51:21 2013 +0200
    31.2 +++ b/src/Pure/Isar/typedecl.ML	Wed Apr 10 19:14:47 2013 +0200
    31.3 @@ -29,7 +29,7 @@
    31.4  fun object_logic_arity name thy =
    31.5    (case Object_Logic.get_base_sort thy of
    31.6      NONE => thy
    31.7 -  | SOME S => AxClass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
    31.8 +  | SOME S => Axclass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
    31.9  
   31.10  fun basic_decl decl (b, n, mx) lthy =
   31.11    let val name = Local_Theory.full_name lthy b in
    32.1 --- a/src/Pure/ML/ml_antiquote.ML	Wed Apr 10 18:51:21 2013 +0200
    32.2 +++ b/src/Pure/ML/ml_antiquote.ML	Wed Apr 10 19:14:47 2013 +0200
    32.3 @@ -76,6 +76,12 @@
    32.4          "Context.get_theory (Proof_Context.theory_of ML_context) " ^ ML_Syntax.print_string name))
    32.5      || Scan.succeed "Proof_Context.theory_of ML_context") #>
    32.6  
    32.7 +  value (Binding.name "theory_context")
    32.8 +    (Args.theory -- Scan.lift (Parse.position Args.name) >> (fn (thy, (name, pos)) =>
    32.9 +      (Position.report pos (Theory.get_markup (Context.get_theory thy name));
   32.10 +        "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
   32.11 +        ML_Syntax.print_string name))) #>
   32.12 +
   32.13    inline (Binding.name "context") (Scan.succeed "Isabelle.ML_context") #>
   32.14  
   32.15    inline (Binding.name "typ") (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
    33.1 --- a/src/Pure/axclass.ML	Wed Apr 10 18:51:21 2013 +0200
    33.2 +++ b/src/Pure/axclass.ML	Wed Apr 10 19:14:47 2013 +0200
    33.3 @@ -5,7 +5,7 @@
    33.4  parameters.  Proven class relations and type arities.
    33.5  *)
    33.6  
    33.7 -signature AX_CLASS =
    33.8 +signature AXCLASS =
    33.9  sig
   33.10    type info = {def: thm, intro: thm, axioms: thm list, params: (string * typ) list}
   33.11    val get_info: theory -> class -> info
   33.12 @@ -38,7 +38,7 @@
   33.13    val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
   33.14  end;
   33.15  
   33.16 -structure AxClass: AX_CLASS =
   33.17 +structure Axclass: AXCLASS =
   33.18  struct
   33.19  
   33.20  (** theory data **)
    34.1 --- a/src/Pure/context.ML	Wed Apr 10 18:51:21 2013 +0200
    34.2 +++ b/src/Pure/context.ML	Wed Apr 10 19:14:47 2013 +0200
    34.3 @@ -21,6 +21,7 @@
    34.4    sig
    34.5      val theory_of: Proof.context -> theory
    34.6      val init_global: theory -> Proof.context
    34.7 +    val get_global: theory -> string -> Proof.context
    34.8    end
    34.9  end;
   34.10  
   34.11 @@ -504,6 +505,7 @@
   34.12  struct
   34.13    val theory_of = theory_of_proof;
   34.14    fun init_global thy = Proof.Context (init_data thy, check_thy thy);
   34.15 +  fun get_global thy name = init_global (get_theory thy name);
   34.16  end;
   34.17  
   34.18  structure Proof_Data =
    35.1 --- a/src/Pure/simplifier.ML	Wed Apr 10 18:51:21 2013 +0200
    35.2 +++ b/src/Pure/simplifier.ML	Wed Apr 10 19:14:47 2013 +0200
    35.3 @@ -10,7 +10,6 @@
    35.4    include BASIC_RAW_SIMPLIFIER
    35.5    val map_simpset: (simpset -> simpset) -> Proof.context -> Proof.context
    35.6    val simpset_of: Proof.context -> simpset
    35.7 -  val global_simpset_of: theory -> simpset
    35.8    val Addsimprocs: simproc list -> unit
    35.9    val Delsimprocs: simproc list -> unit
   35.10    val simp_tac: simpset -> int -> tactic
   35.11 @@ -169,8 +168,6 @@
   35.12  (* global simpset *)
   35.13  
   35.14  fun map_simpset_global f = Context.theory_map (map_ss f);
   35.15 -fun global_simpset_of thy =
   35.16 -  Raw_Simplifier.context (Proof_Context.init_global thy) (get_ss (Context.Theory thy));
   35.17  
   35.18  fun Addsimprocs args = Context.>> (map_ss (fn ss => ss addsimprocs args));
   35.19  fun Delsimprocs args = Context.>> (map_ss (fn ss => ss delsimprocs args));
    36.1 --- a/src/Tools/Code/code_preproc.ML	Wed Apr 10 18:51:21 2013 +0200
    36.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Apr 10 19:14:47 2013 +0200
    36.3 @@ -143,7 +143,7 @@
    36.4      val pre = (Simplifier.global_context thy o #pre o the_thmproc) thy;
    36.5    in
    36.6      Simplifier.rewrite pre
    36.7 -    #> trans_conv_rule (AxClass.unoverload_conv thy)
    36.8 +    #> trans_conv_rule (Axclass.unoverload_conv thy)
    36.9    end;
   36.10  
   36.11  fun preprocess_term thy = term_of_conv_resubst thy (preprocess_conv thy);
   36.12 @@ -152,7 +152,7 @@
   36.13    let
   36.14      val post = (Simplifier.global_context thy o #post o the_thmproc) thy;
   36.15    in
   36.16 -    AxClass.overload_conv thy
   36.17 +    Axclass.overload_conv thy
   36.18      #> trans_conv_rule (Simplifier.rewrite post)
   36.19    end;
   36.20  
   36.21 @@ -213,14 +213,14 @@
   36.22  
   36.23  (* auxiliary *)
   36.24  
   36.25 -fun is_proper_class thy = can (AxClass.get_info thy);
   36.26 +fun is_proper_class thy = can (Axclass.get_info thy);
   36.27  
   36.28  fun complete_proper_sort thy =
   36.29    Sign.complete_sort thy #> filter (is_proper_class thy);
   36.30  
   36.31  fun inst_params thy tyco =
   36.32 -  map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
   36.33 -    o maps (#params o AxClass.get_info thy);
   36.34 +  map (fn (c, _) => Axclass.param_of_inst thy (c, tyco))
   36.35 +    o maps (#params o Axclass.get_info thy);
   36.36  
   36.37  
   36.38  (* data structures *)
    37.1 --- a/src/Tools/Code/code_target.ML	Wed Apr 10 18:51:21 2013 +0200
    37.2 +++ b/src/Tools/Code/code_target.ML	Wed Apr 10 19:14:47 2013 +0200
    37.3 @@ -544,7 +544,7 @@
    37.4  
    37.5  fun cert_class thy class =
    37.6    let
    37.7 -    val _ = AxClass.get_info thy class;
    37.8 +    val _ = Axclass.get_info thy class;
    37.9    in class end;
   37.10  
   37.11  fun read_class thy = cert_class thy o Sign.intern_class thy;
    38.1 --- a/src/Tools/Code/code_thingol.ML	Wed Apr 10 18:51:21 2013 +0200
    38.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Apr 10 19:14:47 2013 +0200
    38.3 @@ -269,10 +269,10 @@
    38.4  local
    38.5    fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
    38.6    fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
    38.7 -  fun thyname_of_instance thy inst = case AxClass.thynames_of_arity thy inst
    38.8 +  fun thyname_of_instance thy inst = case Axclass.thynames_of_arity thy inst
    38.9     of [] => error ("No such instance: " ^ quote (snd inst ^ " :: " ^ fst inst))
   38.10      | thyname :: _ => thyname;
   38.11 -  fun thyname_of_const thy c = case AxClass.class_of_param thy c
   38.12 +  fun thyname_of_const thy c = case Axclass.class_of_param thy c
   38.13     of SOME class => thyname_of_class thy class
   38.14      | NONE => (case Code.get_type_of_constr_or_abstr thy c
   38.15         of SOME (tyco, _) => thyname_of_type thy tyco
   38.16 @@ -662,14 +662,14 @@
   38.17        end;
   38.18      val stmt_const = case Code.get_type_of_constr_or_abstr thy c
   38.19       of SOME (tyco, _) => stmt_datatypecons tyco
   38.20 -      | NONE => (case AxClass.class_of_param thy c
   38.21 +      | NONE => (case Axclass.class_of_param thy c
   38.22           of SOME class => stmt_classparam class
   38.23            | NONE => stmt_fun (Code_Preproc.cert eqngr c))
   38.24    in ensure_stmt lookup_const (declare_const thy) stmt_const c end
   38.25  and ensure_class thy (algbr as (_, algebra)) eqngr permissive class =
   38.26    let
   38.27      val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
   38.28 -    val cs = #params (AxClass.get_info thy class);
   38.29 +    val cs = #params (Axclass.get_info thy class);
   38.30      val stmt_class =
   38.31        fold_map (fn super_class => ensure_class thy algbr eqngr permissive super_class
   38.32          ##>> ensure_classrel thy algbr eqngr permissive (class, super_class)) super_classes
   38.33 @@ -687,7 +687,7 @@
   38.34  and ensure_inst thy (algbr as (_, algebra)) eqngr permissive (class, tyco) =
   38.35    let
   38.36      val super_classes = (Sorts.minimize_sort algebra o Sorts.super_classes algebra) class;
   38.37 -    val these_class_params = these o try (#params o AxClass.get_info thy);
   38.38 +    val these_class_params = these o try (#params o Axclass.get_info thy);
   38.39      val class_params = these_class_params class;
   38.40      val superclass_params = maps these_class_params
   38.41        ((Sorts.complete_sort algebra o Sorts.super_classes algebra) class);
   38.42 @@ -706,7 +706,7 @@
   38.43      fun translate_classparam_instance (c, ty) =
   38.44        let
   38.45          val raw_const = Const (c, map_type_tfree (K arity_typ') ty);
   38.46 -        val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy raw_const);
   38.47 +        val thm = Axclass.unoverload_conv thy (Thm.cterm_of thy raw_const);
   38.48          val const = (apsnd Logic.unvarifyT_global o dest_Const o snd
   38.49            o Logic.dest_equals o Thm.prop_of) thm;
   38.50        in
    39.1 --- a/src/Tools/nbe.ML	Wed Apr 10 18:51:21 2013 +0200
    39.2 +++ b/src/Tools/nbe.ML	Wed Apr 10 19:14:47 2013 +0200
    39.3 @@ -56,7 +56,7 @@
    39.4       of SOME T_class => T_class
    39.5        | _ => error ("Bad certificate: " ^ Display.string_of_thm_global thy thm);
    39.6      val tvar = case try Term.dest_TVar T
    39.7 -     of SOME (tvar as (_, sort)) => if null (filter (can (AxClass.get_info thy)) sort)
    39.8 +     of SOME (tvar as (_, sort)) => if null (filter (can (Axclass.get_info thy)) sort)
    39.9            then tvar
   39.10            else error ("Bad sort: " ^ Display.string_of_thm_global thy thm)
   39.11        | _ => error ("Bad type: " ^ Display.string_of_thm_global thy thm);
   39.12 @@ -65,11 +65,11 @@
   39.13      val lhs_rhs = case try Logic.dest_equals eqn
   39.14       of SOME lhs_rhs => lhs_rhs
   39.15        | _ => error ("Not an equation: " ^ Syntax.string_of_term_global thy eqn);
   39.16 -    val c_c' = case try (pairself (AxClass.unoverload_const thy o dest_Const)) lhs_rhs
   39.17 +    val c_c' = case try (pairself (Axclass.unoverload_const thy o dest_Const)) lhs_rhs
   39.18       of SOME c_c' => c_c'
   39.19        | _ => error ("Not an equation with two constants: "
   39.20            ^ Syntax.string_of_term_global thy eqn);
   39.21 -    val _ = if the_list (AxClass.class_of_param thy (snd c_c')) = [class] then ()
   39.22 +    val _ = if the_list (Axclass.class_of_param thy (snd c_c')) = [class] then ()
   39.23        else error ("Inconsistent class: " ^ Display.string_of_thm_global thy thm);
   39.24    in Triv_Class_Data.map (AList.update (op =) (class, thm)) thy end;
   39.25  
    40.1 --- a/src/ZF/IntDiv_ZF.thy	Wed Apr 10 18:51:21 2013 +0200
    40.2 +++ b/src/ZF/IntDiv_ZF.thy	Wed Apr 10 19:14:47 2013 +0200
    40.3 @@ -1712,7 +1712,7 @@
    40.4             (if ~b | #0 $<= integ_of w
    40.5              then integ_of v zdiv (integ_of w)
    40.6              else (integ_of v $+ #1) zdiv (integ_of w))"
    40.7 - apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT)
    40.8 + apply (simp_tac (simpset_of @{theory_context Int} add: zadd_assoc integ_of_BIT)
    40.9   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)
   40.10   done
   40.11  
   40.12 @@ -1758,7 +1758,7 @@
   40.13                   then #2 $* (integ_of v zmod integ_of w) $+ #1
   40.14                   else #2 $* ((integ_of v $+ #1) zmod integ_of w) - #1
   40.15              else #2 $* (integ_of v zmod integ_of w))"
   40.16 - apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT)
   40.17 + apply (simp_tac (simpset_of @{theory_context Int} add: zadd_assoc integ_of_BIT)
   40.18   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)
   40.19   done
   40.20