# HG changeset patch
# User wenzelm
# Date 1267960787 -3600
# Node ID 9c818cab0dd0d855c0db78413ffc53ca4ca17735
# Parent  c4e29a0bb8c1afbe3f1451dd5decde649a62729c
modernized structure Object_Logic;

diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Boogie/Tools/boogie_loader.ML
--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -87,8 +87,8 @@
       | NONE =>
           let
             val args = Name.variant_list [] (replicate arity "'")
-            val (T, thy') = ObjectLogic.typedecl (Binding.name isa_name, args,
-              mk_syntax name arity) thy
+            val (T, thy') =
+              Object_Logic.typedecl (Binding.name isa_name, args, mk_syntax name arity) thy
             val type_name = fst (Term.dest_Type T)
           in (((name, type_name), log_new name type_name), thy') end)
     end
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Mar 07 12:19:47 2010 +0100
@@ -3098,7 +3098,7 @@
 struct
 
 fun frpar_tac T ps ctxt i = 
- (ObjectLogic.full_atomize_tac i) 
+ Object_Logic.full_atomize_tac i
  THEN (fn st =>
   let
     val g = List.nth (cprems_of st, i - 1)
@@ -3108,7 +3108,7 @@
   in rtac (th RS iffD2) i st end);
 
 fun frpar2_tac T ps ctxt i = 
- (ObjectLogic.full_atomize_tac i) 
+ Object_Logic.full_atomize_tac i
  THEN (fn st =>
   let
     val g = List.nth (cprems_of st, i - 1)
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Decision_Procs/cooper_tac.ML
--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -66,7 +66,7 @@
 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
 
 
-fun linz_tac ctxt q i = ObjectLogic.atomize_prems_tac i THEN (fn st =>
+fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st =>
   let
     val g = List.nth (prems_of st, i - 1)
     val thy = ProofContext.theory_of ctxt
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Decision_Procs/ferrack_tac.ML
--- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -73,7 +73,7 @@
 
 
 fun linr_tac ctxt q =
-    ObjectLogic.atomize_prems_tac
+    Object_Logic.atomize_prems_tac
         THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
         THEN' SUBGOAL (fn (g, i) =>
   let
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Decision_Procs/mir_tac.ML
--- a/src/HOL/Decision_Procs/mir_tac.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -88,7 +88,7 @@
 
 
 fun mir_tac ctxt q i = 
-    ObjectLogic.atomize_prems_tac i
+    Object_Logic.atomize_prems_tac i
         THEN simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i
         THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i)
         THEN (fn st =>
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/HOL.thy	Sun Mar 07 12:19:47 2010 +0100
@@ -44,7 +44,7 @@
 
 classes type
 defaultsort type
-setup {* ObjectLogic.add_base_sort @{sort type} *}
+setup {* Object_Logic.add_base_sort @{sort type} *}
 
 arities
   "fun" :: (type, type) type
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Library/Efficient_Nat.thy
--- a/src/HOL/Library/Efficient_Nat.thy	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Library/Efficient_Nat.thy	Sun Mar 07 12:19:47 2010 +0100
@@ -181,7 +181,7 @@
       | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
       | find_var _ = NONE;
     fun find_thm th =
-      let val th' = Conv.fconv_rule ObjectLogic.atomize th
+      let val th' = Conv.fconv_rule Object_Logic.atomize th
       in Option.map (pair (th, th')) (find_var (prop_of th')) end
   in
     case get_first find_thm thms of
@@ -189,7 +189,7 @@
     | SOME ((th, th'), (Sucv, v)) =>
         let
           val cert = cterm_of (Thm.theory_of_thm th);
-          val th'' = ObjectLogic.rulify (Thm.implies_elim
+          val th'' = Object_Logic.rulify (Thm.implies_elim
             (Conv.fconv_rule (Thm.beta_conversion true)
               (Drule.instantiate' []
                 [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -1431,7 +1431,7 @@
 fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
 
 fun sos_tac print_cert prover ctxt =
-  ObjectLogic.full_atomize_tac THEN'
+  Object_Logic.full_atomize_tac THEN'
   elim_denom_tac ctxt THEN'
   core_sos_tac print_cert prover ctxt;
 
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Library/normarith.ML
--- a/src/HOL/Library/normarith.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Library/normarith.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -410,7 +410,7 @@
 
  fun norm_arith_tac ctxt = 
    clarify_tac HOL_cs THEN'
-   ObjectLogic.full_atomize_tac THEN'
+   Object_Logic.full_atomize_tac THEN'
    CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
 
 end;
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -494,7 +494,7 @@
 fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
  | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T);
 
-fun preprocess thy insts t = ObjectLogic.atomize_term thy
+fun preprocess thy insts t = Object_Logic.atomize_term thy
  (map_types (inst_type insts) (freeze t));
 
 fun is_executable thy insts th =
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -91,7 +91,7 @@
 fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
   | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T)
 
-fun preprocess thy insts t = ObjectLogic.atomize_term thy
+fun preprocess thy insts t = Object_Logic.atomize_term thy
  (map_types (inst_type insts) (Mutabelle.freeze t));
 
 fun invoke_quickcheck quickcheck_generator thy t =
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/NSA/transfer.ML
--- a/src/HOL/NSA/transfer.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/NSA/transfer.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -63,7 +63,7 @@
     val u = unstar_term consts t'
     val tac =
       rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
-      ALLGOALS ObjectLogic.full_atomize_tac THEN
+      ALLGOALS Object_Logic.full_atomize_tac THEN
       match_tac [transitive_thm] 1 THEN
       resolve_tac [@{thm transfer_start}] 1 THEN
       REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -1074,7 +1074,7 @@
       (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
       (fn {prems, ...} => EVERY
         [rtac indrule_lemma' 1,
-         (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+         (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
          EVERY (map (fn (prem, r) => (EVERY
            [REPEAT (eresolve_tac Abs_inverse_thms' 1),
             simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/Datatype/datatype.ML
--- a/src/HOL/Tools/Datatype/datatype.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -417,7 +417,7 @@
 
         val inj_thm = Skip_Proof.prove_global thy5 [] []
           (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
-            [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+            [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
              REPEAT (EVERY
                [rtac allI 1, rtac impI 1,
                 exh_tac (exh_thm_of dt_info) 1,
@@ -443,7 +443,7 @@
         val elem_thm = 
             Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
               (fn _ =>
-               EVERY [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+               EVERY [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
                 rewrite_goals_tac rewrites,
                 REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
                   ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
@@ -479,7 +479,7 @@
     val iso_thms = if length descr = 1 then [] else
       drop (length newTs) (split_conj_thm
         (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
-           [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+           [(indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
             REPEAT (rtac TrueI 1),
             rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
               symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
@@ -617,7 +617,7 @@
       (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
       (fn {prems, ...} => EVERY
         [rtac indrule_lemma' 1,
-         (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
+         (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
          EVERY (map (fn (prem, r) => (EVERY
            [REPEAT (eresolve_tac Abs_inverse_thms 1),
             simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -209,7 +209,7 @@
         val induct' = cterm_instantiate ((map cert induct_Ps) ~~
           (map cert insts)) induct;
         val (tac, _) = fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
-           (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
+           (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1
               THEN rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
 
       in split_conj_thm (Skip_Proof.prove_global thy1 [] []
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/Datatype/datatype_realizer.ML
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -115,7 +115,7 @@
       (fn prems =>
          [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
           rtac (cterm_instantiate inst induct) 1,
-          ALLGOALS ObjectLogic.atomize_prems_tac,
+          ALLGOALS Object_Logic.atomize_prems_tac,
           rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
           REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
             REPEAT (etac allE i) THEN atac i)) 1)]);
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/Function/induction_schema.ML
--- a/src/HOL/Tools/Function/induction_schema.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/Function/induction_schema.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -195,7 +195,7 @@
       |> fold_rev (curry Logic.mk_implies) Cs
       |> fold_rev (Logic.all o Free) ws
       |> term_conv thy ind_atomize
-      |> ObjectLogic.drop_judgment thy
+      |> Object_Logic.drop_judgment thy
       |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   in
     SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/Function/termination.ML
--- a/src/HOL/Tools/Function/termination.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/Function/termination.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -282,7 +282,7 @@
       let
         val (vars, prems, lhs, rhs) = dest_term ineq
       in
-        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems)
+        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term thy) prems)
       end
 
     val relation =
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/Groebner_Basis/groebner.ML
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -967,10 +967,11 @@
           (semiring_normalize_wrapper ctxt res)) form));
 
 fun ring_tac add_ths del_ths ctxt =
-  ObjectLogic.full_atomize_tac
-  THEN' asm_full_simp_tac (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths)
+  Object_Logic.full_atomize_tac
+  THEN' asm_full_simp_tac
+    (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths)
   THEN' CSUBGOAL (fn (p, i) =>
-    rtac (let val form = (ObjectLogic.dest_judgment p)
+    rtac (let val form = Object_Logic.dest_judgment p
           in case get_ring_ideal_convs ctxt form of
            NONE => reflexive form
           | SOME thy => #ring_conv thy form
@@ -1008,7 +1009,7 @@
    end
   in  
      clarify_tac @{claset} i 
-     THEN ObjectLogic.full_atomize_tac i 
+     THEN Object_Logic.full_atomize_tac i 
      THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i 
      THEN clarify_tac @{claset} i 
      THEN (REPEAT (CONVERSION (#unwind_conv thy) i))
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/Nitpick/minipick.ML
--- a/src/HOL/Tools/Nitpick/minipick.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/minipick.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -298,7 +298,7 @@
       | card (Type ("*", [T1, T2])) = card T1 * card T2
       | card @{typ bool} = 2
       | card T = Int.max (1, raw_card T)
-    val neg_t = @{const Not} $ ObjectLogic.atomize_term thy t
+    val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
     val _ = fold_types (K o check_type ctxt) neg_t ()
     val frees = Term.add_frees neg_t []
     val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -1762,8 +1762,8 @@
 (* theory -> styp -> term -> term list * term list * term *)
 fun triple_for_intro_rule thy x t =
   let
-    val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
-    val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
+    val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term thy)
+    val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term thy
     val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
     (* term -> bool *)
      val is_good_head = curry (op =) (Const x) o head_of
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -807,7 +807,7 @@
     fun try_out negate =
       let
         val concl = (negate ? curry (op $) @{const Not})
-                    (ObjectLogic.atomize_term thy prop)
+                    (Object_Logic.atomize_term thy prop)
         val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
                    |> map_types (map_type_tfree
                                      (fn (s, []) => TFree (s, HOLogic.typeS)
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/Qelim/ferrante_rackoff.ML
--- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -225,9 +225,9 @@
   (case dlo_instance ctxt p of
     NONE => no_tac
   | SOME instance =>
-      ObjectLogic.full_atomize_tac i THEN
+      Object_Logic.full_atomize_tac i THEN
       simp_tac (#simpset (snd instance)) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
-      CONVERSION (ObjectLogic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
+      CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
       simp_tac (simpset_of ctxt) i));  (* FIXME really? *)
 
 end;
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/Qelim/langford.ML
--- a/src/HOL/Tools/Qelim/langford.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/Qelim/langford.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -234,11 +234,11 @@
   (case dlo_instance ctxt p of
     (ss, NONE) => simp_tac ss i
   | (ss,  SOME instance) =>
-      ObjectLogic.full_atomize_tac i THEN
+      Object_Logic.full_atomize_tac i THEN
       simp_tac ss i
       THEN (CONVERSION Thm.eta_long_conversion) i
       THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
-      THEN ObjectLogic.full_atomize_tac i
-      THEN CONVERSION (ObjectLogic.judgment_conv (raw_dlo_conv ss instance)) i
+      THEN Object_Logic.full_atomize_tac i
+      THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ss instance)) i
       THEN (simp_tac ss i)));  
 end;
\ No newline at end of file
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/Qelim/presburger.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -166,13 +166,13 @@
     val aprems = Arith_Data.get_arith_facts ctxt
 in
   Method.insert_tac aprems
-  THEN_ALL_NEW ObjectLogic.full_atomize_tac
+  THEN_ALL_NEW Object_Logic.full_atomize_tac
   THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   THEN_ALL_NEW simp_tac ss
   THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
-  THEN_ALL_NEW ObjectLogic.full_atomize_tac
+  THEN_ALL_NEW Object_Logic.full_atomize_tac
   THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
-  THEN_ALL_NEW ObjectLogic.full_atomize_tac
+  THEN_ALL_NEW Object_Logic.full_atomize_tac
   THEN_ALL_NEW div_mod_tac ctxt
   THEN_ALL_NEW splits_tac ctxt
   THEN_ALL_NEW simp_tac ss
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -48,7 +48,7 @@
 fun atomize_thm thm =
 let
   val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
-  val thm'' = ObjectLogic.atomize (cprop_of thm')
+  val thm'' = Object_Logic.atomize (cprop_of thm')
 in
   @{thm equal_elim_rule1} OF [thm'', thm']
 end
@@ -616,7 +616,7 @@
 
 (* the tactic leaves three subgoals to be proved *)
 fun procedure_tac ctxt rthm =
-  ObjectLogic.full_atomize_tac
+  Object_Logic.full_atomize_tac
   THEN' gen_frees_tac ctxt
   THEN' SUBGOAL (fn (goal, i) =>
     let
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -151,9 +151,9 @@
                {f = f, R = R, rules = rules,
                 full_pats_TCs = full_pats_TCs,
                 TCs = TCs}
-       val rules' = map (Drule.export_without_context o ObjectLogic.rulify_no_asm)
+       val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
                         (R.CONJUNCTS rules)
-         in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
+         in  {induct = meta_outer (Object_Logic.rulify_no_asm (induction RS spec')),
         rules = ListPair.zip(rules', rows),
         tcs = (termination_goals rules') @ tcs}
    end
@@ -180,7 +180,7 @@
     | solve_eq (th, [a], i) = [(a, i)]
     | solve_eq (th, splitths as (_ :: _), i) = 
       (writeln "Proving unsplit equation...";
-      [((Drule.export_without_context o ObjectLogic.rulify_no_asm)
+      [((Drule.export_without_context o Object_Logic.rulify_no_asm)
           (CaseSplit.splitto splitths th), i)])
       (* if there's an error, pretend nothing happened with this definition 
          We should probably print something out so that the user knows...? *)
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/choice_specification.ML
--- a/src/HOL/Tools/choice_specification.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/choice_specification.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -111,7 +111,7 @@
           | myfoldr f [] = error "Choice_Specification.process_spec internal error"
 
         val rew_imps = alt_props |>
-          map (ObjectLogic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
+          map (Object_Logic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
         val props' = rew_imps |>
           map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
 
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/hologic.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -190,14 +190,14 @@
 
 fun conj_intr thP thQ =
   let
-    val (P, Q) = pairself (ObjectLogic.dest_judgment o Thm.cprop_of) (thP, thQ)
+    val (P, Q) = pairself (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ)
       handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
     val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
   in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
 
 fun conj_elim thPQ =
   let
-    val (P, Q) = Thm.dest_binop (ObjectLogic.dest_judgment (Thm.cprop_of thPQ))
+    val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment (Thm.cprop_of thPQ))
       handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
     val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
     val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/inductive.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -788,7 +788,7 @@
        else if coind then
          singleton (ProofContext.export
            (snd (Variable.add_fixes (map (fst o dest_Free) params) lthy1)) lthy1)
-           (rotate_prems ~1 (ObjectLogic.rulify
+           (rotate_prems ~1 (Object_Logic.rulify
              (fold_rule rec_preds_defs
                (rewrite_rule simp_thms'''
                 (mono RS (fp_def RS @{thm def_coinduct}))))))
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/inductive_realizer.ML
--- a/src/HOL/Tools/inductive_realizer.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -395,7 +395,7 @@
           [rtac (#raw_induct ind_info) 1,
            rewrite_goals_tac rews,
            REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
-             [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
+             [K (rewrite_goals_tac rews), Object_Logic.atomize_prems_tac,
               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
         val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
           (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
@@ -454,7 +454,7 @@
            etac elimR 1,
            ALLGOALS (asm_simp_tac HOL_basic_ss),
            rewrite_goals_tac rews,
-           REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
+           REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac THEN'
              DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
         val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
           (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -901,7 +901,7 @@
 in
 
 fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
-  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
+  Object_Logic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
 
 val tac = gen_tac true;
 
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/meson.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -587,7 +587,7 @@
   Function mkcl converts theorems to clauses.*)
 fun MESON mkcl cltac ctxt i st =
   SELECT_GOAL
-    (EVERY [ObjectLogic.atomize_prems_tac 1,
+    (EVERY [Object_Logic.atomize_prems_tac 1,
             rtac ccontr 1,
             Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
                       EVERY1 [skolemize_prems_tac ctxt negs,
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/record.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -2214,7 +2214,7 @@
             [(cterm_of defs_thy Pvar, cterm_of defs_thy
               (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
             induct_scheme;
-        in ObjectLogic.rulify (mp OF [ind, refl]) end;
+        in Object_Logic.rulify (mp OF [ind, refl]) end;
 
     val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
     val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -276,7 +276,7 @@
   let val th1 = th |> transform_elim |> zero_var_indexes
       val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
       val th3 = th2
-        |> Conv.fconv_rule ObjectLogic.atomize
+        |> Conv.fconv_rule Object_Logic.atomize
         |> Meson.make_nnf ctxt |> strip_lambdas ~1
   in  (th3, ctxt)  end;
 
@@ -493,7 +493,7 @@
 (*** Converting a subgoal into negated conjecture clauses. ***)
 
 fun neg_skolemize_tac ctxt =
-  EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac ctxt];
+  EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
 
 val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
 
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/sat_funcs.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -434,7 +434,7 @@
 
 val pre_cnf_tac =
         rtac ccontr THEN'
-        ObjectLogic.atomize_prems_tac THEN'
+        Object_Logic.atomize_prems_tac THEN'
         CONVERSION Drule.beta_eta_conversion;
 
 (* ------------------------------------------------------------------------- *)
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/HOL/Tools/typedef.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -130,7 +130,7 @@
           in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
 
     fun typedef_result inhabited =
-      ObjectLogic.typedecl (tname, vs, mx)
+      Object_Logic.typedecl (tname, vs, mx)
       #> snd
       #> Sign.add_consts_i
         [(Rep_name, newT --> oldT, NoSyn),
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Provers/blast.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -181,7 +181,7 @@
 fun isGoal (Const ("*Goal*", _) $ _) = true
   | isGoal _ = false;
 
-val TruepropC = ObjectLogic.judgment_name Data.thy;
+val TruepropC = Object_Logic.judgment_name Data.thy;
 val TruepropT = Sign.the_const_type Data.thy TruepropC;
 
 fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
@@ -1251,7 +1251,7 @@
 fun timing_depth_tac start cs lim i st0 =
   let val thy = Thm.theory_of_thm st0
       val state = initialize thy
-      val st = Conv.gconv_rule ObjectLogic.atomize_prems i st0
+      val st = Conv.gconv_rule Object_Logic.atomize_prems i st0
       val skoprem = fromSubgoal thy (List.nth(prems_of st, i-1))
       val hyps  = strip_imp_prems skoprem
       and concl = strip_imp_concl skoprem
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Provers/classical.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -153,7 +153,7 @@
 *)
 
 fun classical_rule rule =
-  if ObjectLogic.is_elim rule then
+  if Object_Logic.is_elim rule then
     let
       val rule' = rule RS classical;
       val concl' = Thm.concl_of rule';
@@ -173,7 +173,7 @@
   else rule;
 
 (*flatten nested meta connectives in prems*)
-val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 ObjectLogic.atomize_prems);
+val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems);
 
 
 (*** Useful tactics for classical reasoning ***)
@@ -724,24 +724,24 @@
 
 (*Dumb but fast*)
 fun fast_tac cs =
-  ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
+  Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
 
 (*Slower but smarter than fast_tac*)
 fun best_tac cs =
-  ObjectLogic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
 
 (*even a bit smarter than best_tac*)
 fun first_best_tac cs =
-  ObjectLogic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
 
 fun slow_tac cs =
-  ObjectLogic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
 
 fun slow_best_tac cs =
-  ObjectLogic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
 
 
@@ -749,13 +749,13 @@
 val weight_ASTAR = Unsynchronized.ref 5;
 
 fun astar_tac cs =
-  ObjectLogic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL
     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
       (step_tac cs 1));
 
 fun slow_astar_tac cs =
-  ObjectLogic.atomize_prems_tac THEN'
+  Object_Logic.atomize_prems_tac THEN'
   SELECT_GOAL
     (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
       (slow_step_tac cs 1));
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Provers/splitter.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -46,14 +46,14 @@
 struct
 
 val Const (const_not, _) $ _ =
-  ObjectLogic.drop_judgment Data.thy
+  Object_Logic.drop_judgment Data.thy
     (#1 (Logic.dest_implies (Thm.prop_of Data.notnotD)));
 
 val Const (const_or , _) $ _ $ _ =
-  ObjectLogic.drop_judgment Data.thy
+  Object_Logic.drop_judgment Data.thy
     (#1 (Logic.dest_implies (Thm.prop_of Data.disjE)));
 
-val const_Trueprop = ObjectLogic.judgment_name Data.thy;
+val const_Trueprop = Object_Logic.judgment_name Data.thy;
 
 
 fun split_format_err () = error "Wrong format for split rule";
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -252,7 +252,7 @@
 (* rule format *)
 
 val rule_format = Args.mode "no_asm"
-  >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format);
+  >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format);
 
 val elim_format = Thm.rule_attribute (K Tactic.make_elim);
 
@@ -306,9 +306,9 @@
   setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
   setup (Binding.name "eta_long") (Scan.succeed eta_long)
     "put theorem into eta long beta normal form" #>
-  setup (Binding.name "atomize") (Scan.succeed ObjectLogic.declare_atomize)
+  setup (Binding.name "atomize") (Scan.succeed Object_Logic.declare_atomize)
     "declaration of atomize rule" #>
-  setup (Binding.name "rulify") (Scan.succeed ObjectLogic.declare_rulify)
+  setup (Binding.name "rulify") (Scan.succeed Object_Logic.declare_rulify)
     "declaration of rulify rule" #>
   setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
   setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Pure/Isar/auto_bind.ML
--- a/src/Pure/Isar/auto_bind.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Isar/auto_bind.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -23,7 +23,7 @@
 val thisN = "this";
 val assmsN = "assms";
 
-fun strip_judgment thy = ObjectLogic.drop_judgment thy o Logic.strip_assums_concl;
+fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl;
 
 fun statement_binds thy name prop =
   [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Isar/element.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -223,12 +223,12 @@
     val cert = Thm.cterm_of thy;
 
     val th = MetaSimplifier.norm_hhf raw_th;
-    val is_elim = ObjectLogic.is_elim th;
+    val is_elim = Object_Logic.is_elim th;
 
     val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt);
     val prop = Thm.prop_of th';
     val (prems, concl) = Logic.strip_horn prop;
-    val concl_term = ObjectLogic.drop_judgment thy concl;
+    val concl_term = Object_Logic.drop_judgment thy concl;
 
     val fixes = fold_aterms (fn v as Free (x, T) =>
         if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -595,11 +595,11 @@
 fun atomize_spec thy ts =
   let
     val t = Logic.mk_conjunction_balanced ts;
-    val body = ObjectLogic.atomize_term thy t;
+    val body = Object_Logic.atomize_term thy t;
     val bodyT = Term.fastype_of body;
   in
     if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
-    else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
+    else (body, bodyT, Object_Logic.atomize (Thm.cterm_of thy t))
   end;
 
 (* achieve plain syntax for locale predicates (without "PROP") *)
@@ -634,7 +634,7 @@
 
     val args = map Logic.mk_type extraTs @ map Free xs;
     val head = Term.list_comb (Const (name, predT), args);
-    val statement = ObjectLogic.ensure_propT thy head;
+    val statement = Object_Logic.ensure_propT thy head;
 
     val ([pred_def], defs_thy) =
       thy
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -105,7 +105,7 @@
 val _ =
   OuterSyntax.command "typedecl" "type declaration" K.thy_decl
     (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
-      Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd)));
+      Toplevel.theory (Object_Logic.typedecl (a, args, mx) #> snd)));
 
 val _ =
   OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
@@ -127,7 +127,7 @@
 
 val _ =
   OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
-    (P.const_binding >> (Toplevel.theory o ObjectLogic.add_judgment_cmd));
+    (P.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
 
 val _ =
   OuterSyntax.command "consts" "declare constants" K.thy_decl
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Isar/method.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -171,8 +171,8 @@
 
 (* atomize rule statements *)
 
-fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_prems_tac)
-  | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
+fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac)
+  | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac)));
 
 
 (* this -- resolve facts directly *)
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Pure/Isar/object_logic.ML
--- a/src/Pure/Isar/object_logic.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Isar/object_logic.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -34,7 +34,7 @@
   val rule_format_no_asm: attribute
 end;
 
-structure ObjectLogic: OBJECT_LOGIC =
+structure Object_Logic: OBJECT_LOGIC =
 struct
 
 (** theory data **)
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Pure/Isar/obtain.ML
--- a/src/Pure/Isar/obtain.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Isar/obtain.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -76,7 +76,7 @@
     val thy = ProofContext.theory_of fix_ctxt;
 
     val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
-    val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse
+    val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse
       error "Conclusion in obtained context must be object-logic judgment";
 
     val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
@@ -100,7 +100,7 @@
 fun bind_judgment ctxt name =
   let
     val (bind, ctxt') = ProofContext.bind_fixes [name] ctxt;
-    val (t as _ $ Free v) = bind (ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name);
+    val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) name);
   in ((v, t), ctxt') end;
 
 val thatN = "that";
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -110,7 +110,7 @@
         val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) case_outline prop
           |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
 
-        val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop);
+        val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
         val binds =
           (case_conclN, concl) :: dest_binops concls concl
           |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Isar/specification.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -316,7 +316,7 @@
         val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
         val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
 
-        val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
+        val thesis = Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
 
         fun assume_case ((name, (vars, _)), asms) ctxt' =
           let
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Thy/term_style.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -64,8 +64,8 @@
 
 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
   let
-    val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
-      (Logic.strip_imp_concl t)
+    val concl =
+      Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
   in
     case concl of (_ $ l $ r) => proj (l, r)
     | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -93,7 +93,7 @@
 
 (* matching theorems *)
 
-fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy;
+fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
 
 (*educated guesses on HOL*)  (* FIXME broken *)
 val boolT = Type ("bool", []);
@@ -110,13 +110,13 @@
     fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
     fun matches pat =
       let
-        val jpat = ObjectLogic.drop_judgment thy pat;
+        val jpat = Object_Logic.drop_judgment thy pat;
         val c = Term.head_of jpat;
         val pats =
           if Term.is_Const c
           then
             if doiff andalso c = iff_const then
-              (pat :: map (ObjectLogic.ensure_propT thy) (snd (strip_comb jpat)))
+              (pat :: map (Object_Logic.ensure_propT thy) (snd (strip_comb jpat)))
                 |> filter (is_nontrivial thy)
             else [pat]
           else [];
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Pure/old_goals.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -606,11 +606,11 @@
 fun qed_goalw name thy rews goal tacsf =
   ML_Context.ml_store_thm (name, prove_goalw thy rews goal tacsf);
 fun qed_spec_mp name =
-  ML_Context.ml_store_thm (name, ObjectLogic.rulify_no_asm (result ()));
+  ML_Context.ml_store_thm (name, Object_Logic.rulify_no_asm (result ()));
 fun qed_goal_spec_mp name thy s p =
-  bind_thm (name, ObjectLogic.rulify_no_asm (prove_goal thy s p));
+  bind_thm (name, Object_Logic.rulify_no_asm (prove_goal thy s p));
 fun qed_goalw_spec_mp name thy defs s p =
-  bind_thm (name, ObjectLogic.rulify_no_asm (prove_goalw thy defs s p));
+  bind_thm (name, Object_Logic.rulify_no_asm (prove_goalw thy defs s p));
 
 end;
 
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Tools/atomize_elim.ML
--- a/src/Tools/atomize_elim.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Tools/atomize_elim.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -59,9 +59,9 @@
    (EX x y z. ...) | ... | (EX a b c. ...)
 *)
 fun atomize_elim_conv ctxt ct =
-    (forall_conv (K (prems_conv ~1 ObjectLogic.atomize_prems)) ctxt
+    (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
     then_conv MetaSimplifier.rewrite true (AtomizeElimData.get ctxt)
-    then_conv (fn ct' => if can ObjectLogic.dest_judgment ct'
+    then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
                          then all_conv ct'
                          else raise CTERM ("atomize_elim", [ct', ct])))
     ct
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Tools/induct.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -137,7 +137,7 @@
       Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv
       Conv.rewr_conv Drule.swap_prems_eq
 
-fun drop_judgment ctxt = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt);
+fun drop_judgment ctxt = Object_Logic.drop_judgment (ProofContext.theory_of ctxt);
 
 fun find_eq ctxt t =
   let
@@ -511,7 +511,7 @@
 
 fun atomize_term thy =
   MetaSimplifier.rewrite_term thy Data.atomize []
-  #> ObjectLogic.drop_judgment thy;
+  #> Object_Logic.drop_judgment thy;
 
 val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
 
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Tools/induct_tacs.ML
--- a/src/Tools/induct_tacs.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Tools/induct_tacs.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -92,7 +92,7 @@
             (_, rule) :: _ => rule
           | [] => raise THM ("No induction rules", 0, [])));
 
-    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize);
+    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 Object_Logic.atomize);
     val _ = Method.trace ctxt [rule'];
 
     val concls = Logic.dest_conjunctions (Thm.concl_of rule);
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Tools/intuitionistic.ML
--- a/src/Tools/intuitionistic.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Tools/intuitionistic.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -89,7 +89,7 @@
   Method.setup name
     (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
       (fn opt_lim => fn ctxt =>
-        SIMPLE_METHOD' (ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
+        SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
     "intuitionistic proof search";
 
 end;
diff -r c4e29a0bb8c1 -r 9c818cab0dd0 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Sun Mar 07 11:57:16 2010 +0100
+++ b/src/Tools/quickcheck.ML	Sun Mar 07 12:19:47 2010 +0100
@@ -199,7 +199,7 @@
     val gi' = Logic.list_implies (if no_assms then [] else assms,
                                   subst_bounds (frees, strip gi))
       |> monomorphic_term thy insts default_T
-      |> ObjectLogic.atomize_term thy;
+      |> Object_Logic.atomize_term thy;
   in gen_test_term ctxt quiet report generator_name size iterations gi' end;
 
 fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample."