modernized structure Object_Logic;
authorwenzelm
Sun Mar 07 12:19:47 2010 +0100 (2010-03-07)
changeset 356259c818cab0dd0
parent 35624 c4e29a0bb8c1
child 35626 06197484c6ad
modernized structure Object_Logic;
src/HOL/Boogie/Tools/boogie_loader.ML
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/HOL.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/normarith.ML
src/HOL/Mutabelle/mutabelle.ML
src/HOL/Mutabelle/mutabelle_extra.ML
src/HOL/NSA/transfer.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Function/induction_schema.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Groebner_Basis/groebner.ML
src/HOL/Tools/Nitpick/minipick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Qelim/ferrante_rackoff.ML
src/HOL/Tools/Qelim/langford.ML
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/TFL/post.ML
src/HOL/Tools/choice_specification.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_realizer.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/meson.ML
src/HOL/Tools/record.ML
src/HOL/Tools/res_axioms.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/typedef.ML
src/Provers/blast.ML
src/Provers/classical.ML
src/Provers/splitter.ML
src/Pure/Isar/attrib.ML
src/Pure/Isar/auto_bind.ML
src/Pure/Isar/element.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/method.ML
src/Pure/Isar/object_logic.ML
src/Pure/Isar/obtain.ML
src/Pure/Isar/rule_cases.ML
src/Pure/Isar/specification.ML
src/Pure/Thy/term_style.ML
src/Pure/Tools/find_theorems.ML
src/Pure/old_goals.ML
src/Tools/atomize_elim.ML
src/Tools/induct.ML
src/Tools/induct_tacs.ML
src/Tools/intuitionistic.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Mar 07 11:57:16 2010 +0100
     1.2 +++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Sun Mar 07 12:19:47 2010 +0100
     1.3 @@ -87,8 +87,8 @@
     1.4        | NONE =>
     1.5            let
     1.6              val args = Name.variant_list [] (replicate arity "'")
     1.7 -            val (T, thy') = ObjectLogic.typedecl (Binding.name isa_name, args,
     1.8 -              mk_syntax name arity) thy
     1.9 +            val (T, thy') =
    1.10 +              Object_Logic.typedecl (Binding.name isa_name, args, mk_syntax name arity) thy
    1.11              val type_name = fst (Term.dest_Type T)
    1.12            in (((name, type_name), log_new name type_name), thy') end)
    1.13      end
     2.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Mar 07 11:57:16 2010 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun Mar 07 12:19:47 2010 +0100
     2.3 @@ -3098,7 +3098,7 @@
     2.4  struct
     2.5  
     2.6  fun frpar_tac T ps ctxt i = 
     2.7 - (ObjectLogic.full_atomize_tac i) 
     2.8 + Object_Logic.full_atomize_tac i
     2.9   THEN (fn st =>
    2.10    let
    2.11      val g = List.nth (cprems_of st, i - 1)
    2.12 @@ -3108,7 +3108,7 @@
    2.13    in rtac (th RS iffD2) i st end);
    2.14  
    2.15  fun frpar2_tac T ps ctxt i = 
    2.16 - (ObjectLogic.full_atomize_tac i) 
    2.17 + Object_Logic.full_atomize_tac i
    2.18   THEN (fn st =>
    2.19    let
    2.20      val g = List.nth (cprems_of st, i - 1)
     3.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sun Mar 07 11:57:16 2010 +0100
     3.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sun Mar 07 12:19:47 2010 +0100
     3.3 @@ -66,7 +66,7 @@
     3.4  fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
     3.5  
     3.6  
     3.7 -fun linz_tac ctxt q i = ObjectLogic.atomize_prems_tac i THEN (fn st =>
     3.8 +fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st =>
     3.9    let
    3.10      val g = List.nth (prems_of st, i - 1)
    3.11      val thy = ProofContext.theory_of ctxt
     4.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Mar 07 11:57:16 2010 +0100
     4.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Sun Mar 07 12:19:47 2010 +0100
     4.3 @@ -73,7 +73,7 @@
     4.4  
     4.5  
     4.6  fun linr_tac ctxt q =
     4.7 -    ObjectLogic.atomize_prems_tac
     4.8 +    Object_Logic.atomize_prems_tac
     4.9          THEN' (REPEAT_DETERM o split_tac [@{thm split_min}, @{thm split_max}, @{thm abs_split}])
    4.10          THEN' SUBGOAL (fn (g, i) =>
    4.11    let
     5.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Sun Mar 07 11:57:16 2010 +0100
     5.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Sun Mar 07 12:19:47 2010 +0100
     5.3 @@ -88,7 +88,7 @@
     5.4  
     5.5  
     5.6  fun mir_tac ctxt q i = 
     5.7 -    ObjectLogic.atomize_prems_tac i
     5.8 +    Object_Logic.atomize_prems_tac i
     5.9          THEN simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i
    5.10          THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i)
    5.11          THEN (fn st =>
     6.1 --- a/src/HOL/HOL.thy	Sun Mar 07 11:57:16 2010 +0100
     6.2 +++ b/src/HOL/HOL.thy	Sun Mar 07 12:19:47 2010 +0100
     6.3 @@ -44,7 +44,7 @@
     6.4  
     6.5  classes type
     6.6  defaultsort type
     6.7 -setup {* ObjectLogic.add_base_sort @{sort type} *}
     6.8 +setup {* Object_Logic.add_base_sort @{sort type} *}
     6.9  
    6.10  arities
    6.11    "fun" :: (type, type) type
     7.1 --- a/src/HOL/Library/Efficient_Nat.thy	Sun Mar 07 11:57:16 2010 +0100
     7.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Sun Mar 07 12:19:47 2010 +0100
     7.3 @@ -181,7 +181,7 @@
     7.4        | find_var (t $ u) = (case find_var t of NONE => find_var u | x => x)
     7.5        | find_var _ = NONE;
     7.6      fun find_thm th =
     7.7 -      let val th' = Conv.fconv_rule ObjectLogic.atomize th
     7.8 +      let val th' = Conv.fconv_rule Object_Logic.atomize th
     7.9        in Option.map (pair (th, th')) (find_var (prop_of th')) end
    7.10    in
    7.11      case get_first find_thm thms of
    7.12 @@ -189,7 +189,7 @@
    7.13      | SOME ((th, th'), (Sucv, v)) =>
    7.14          let
    7.15            val cert = cterm_of (Thm.theory_of_thm th);
    7.16 -          val th'' = ObjectLogic.rulify (Thm.implies_elim
    7.17 +          val th'' = Object_Logic.rulify (Thm.implies_elim
    7.18              (Conv.fconv_rule (Thm.beta_conversion true)
    7.19                (Drule.instantiate' []
    7.20                  [SOME (cert (lambda v (Abs ("x", HOLogic.natT,
     8.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sun Mar 07 11:57:16 2010 +0100
     8.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Sun Mar 07 12:19:47 2010 +0100
     8.3 @@ -1431,7 +1431,7 @@
     8.4  fun elim_denom_tac ctxt i = REPEAT (elim_one_denom_tac ctxt i);
     8.5  
     8.6  fun sos_tac print_cert prover ctxt =
     8.7 -  ObjectLogic.full_atomize_tac THEN'
     8.8 +  Object_Logic.full_atomize_tac THEN'
     8.9    elim_denom_tac ctxt THEN'
    8.10    core_sos_tac print_cert prover ctxt;
    8.11  
     9.1 --- a/src/HOL/Library/normarith.ML	Sun Mar 07 11:57:16 2010 +0100
     9.2 +++ b/src/HOL/Library/normarith.ML	Sun Mar 07 12:19:47 2010 +0100
     9.3 @@ -410,7 +410,7 @@
     9.4  
     9.5   fun norm_arith_tac ctxt = 
     9.6     clarify_tac HOL_cs THEN'
     9.7 -   ObjectLogic.full_atomize_tac THEN'
     9.8 +   Object_Logic.full_atomize_tac THEN'
     9.9     CSUBGOAL ( fn (p,i) => rtac (norm_arith ctxt (Thm.dest_arg p )) i);
    9.10  
    9.11  end;
    10.1 --- a/src/HOL/Mutabelle/mutabelle.ML	Sun Mar 07 11:57:16 2010 +0100
    10.2 +++ b/src/HOL/Mutabelle/mutabelle.ML	Sun Mar 07 12:19:47 2010 +0100
    10.3 @@ -494,7 +494,7 @@
    10.4  fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
    10.5   | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T);
    10.6  
    10.7 -fun preprocess thy insts t = ObjectLogic.atomize_term thy
    10.8 +fun preprocess thy insts t = Object_Logic.atomize_term thy
    10.9   (map_types (inst_type insts) (freeze t));
   10.10  
   10.11  fun is_executable thy insts th =
    11.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Mar 07 11:57:16 2010 +0100
    11.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Sun Mar 07 12:19:47 2010 +0100
    11.3 @@ -91,7 +91,7 @@
    11.4  fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
    11.5    | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T)
    11.6  
    11.7 -fun preprocess thy insts t = ObjectLogic.atomize_term thy
    11.8 +fun preprocess thy insts t = Object_Logic.atomize_term thy
    11.9   (map_types (inst_type insts) (Mutabelle.freeze t));
   11.10  
   11.11  fun invoke_quickcheck quickcheck_generator thy t =
    12.1 --- a/src/HOL/NSA/transfer.ML	Sun Mar 07 11:57:16 2010 +0100
    12.2 +++ b/src/HOL/NSA/transfer.ML	Sun Mar 07 12:19:47 2010 +0100
    12.3 @@ -63,7 +63,7 @@
    12.4      val u = unstar_term consts t'
    12.5      val tac =
    12.6        rewrite_goals_tac (ths' @ refolds' @ unfolds') THEN
    12.7 -      ALLGOALS ObjectLogic.full_atomize_tac THEN
    12.8 +      ALLGOALS Object_Logic.full_atomize_tac THEN
    12.9        match_tac [transitive_thm] 1 THEN
   12.10        resolve_tac [@{thm transfer_start}] 1 THEN
   12.11        REPEAT_ALL_NEW (resolve_tac intros) 1 THEN
    13.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Sun Mar 07 11:57:16 2010 +0100
    13.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Sun Mar 07 12:19:47 2010 +0100
    13.3 @@ -1074,7 +1074,7 @@
    13.4        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
    13.5        (fn {prems, ...} => EVERY
    13.6          [rtac indrule_lemma' 1,
    13.7 -         (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    13.8 +         (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
    13.9           EVERY (map (fn (prem, r) => (EVERY
   13.10             [REPEAT (eresolve_tac Abs_inverse_thms' 1),
   13.11              simp_tac (HOL_basic_ss addsimps [symmetric r]) 1,
    14.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Mar 07 11:57:16 2010 +0100
    14.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Mar 07 12:19:47 2010 +0100
    14.3 @@ -417,7 +417,7 @@
    14.4  
    14.5          val inj_thm = Skip_Proof.prove_global thy5 [] []
    14.6            (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
    14.7 -            [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    14.8 +            [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
    14.9               REPEAT (EVERY
   14.10                 [rtac allI 1, rtac impI 1,
   14.11                  exh_tac (exh_thm_of dt_info) 1,
   14.12 @@ -443,7 +443,7 @@
   14.13          val elem_thm = 
   14.14              Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
   14.15                (fn _ =>
   14.16 -               EVERY [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
   14.17 +               EVERY [(indtac induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   14.18                  rewrite_goals_tac rewrites,
   14.19                  REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
   14.20                    ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
   14.21 @@ -479,7 +479,7 @@
   14.22      val iso_thms = if length descr = 1 then [] else
   14.23        drop (length newTs) (split_conj_thm
   14.24          (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
   14.25 -           [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
   14.26 +           [(indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   14.27              REPEAT (rtac TrueI 1),
   14.28              rewrite_goals_tac (mk_meta_eq @{thm choice_eq} ::
   14.29                symmetric (mk_meta_eq @{thm expand_fun_eq}) :: range_eqs),
   14.30 @@ -617,7 +617,7 @@
   14.31        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
   14.32        (fn {prems, ...} => EVERY
   14.33          [rtac indrule_lemma' 1,
   14.34 -         (indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
   14.35 +         (indtac rep_induct [] THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1,
   14.36           EVERY (map (fn (prem, r) => (EVERY
   14.37             [REPEAT (eresolve_tac Abs_inverse_thms 1),
   14.38              simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
    15.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Mar 07 11:57:16 2010 +0100
    15.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sun Mar 07 12:19:47 2010 +0100
    15.3 @@ -209,7 +209,7 @@
    15.4          val induct' = cterm_instantiate ((map cert induct_Ps) ~~
    15.5            (map cert insts)) induct;
    15.6          val (tac, _) = fold mk_unique_tac (descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts)
    15.7 -           (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
    15.8 +           (((rtac induct' THEN_ALL_NEW Object_Logic.atomize_prems_tac) 1
    15.9                THEN rewrite_goals_tac [mk_meta_eq @{thm choice_eq}], rec_intrs));
   15.10  
   15.11        in split_conj_thm (Skip_Proof.prove_global thy1 [] []
    16.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Sun Mar 07 11:57:16 2010 +0100
    16.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Sun Mar 07 12:19:47 2010 +0100
    16.3 @@ -115,7 +115,7 @@
    16.4        (fn prems =>
    16.5           [rewrite_goals_tac (map mk_meta_eq [fst_conv, snd_conv]),
    16.6            rtac (cterm_instantiate inst induct) 1,
    16.7 -          ALLGOALS ObjectLogic.atomize_prems_tac,
    16.8 +          ALLGOALS Object_Logic.atomize_prems_tac,
    16.9            rewrite_goals_tac (@{thm o_def} :: map mk_meta_eq rec_rewrites),
   16.10            REPEAT ((resolve_tac prems THEN_ALL_NEW (fn i =>
   16.11              REPEAT (etac allE i) THEN atac i)) 1)]);
    17.1 --- a/src/HOL/Tools/Function/induction_schema.ML	Sun Mar 07 11:57:16 2010 +0100
    17.2 +++ b/src/HOL/Tools/Function/induction_schema.ML	Sun Mar 07 12:19:47 2010 +0100
    17.3 @@ -195,7 +195,7 @@
    17.4        |> fold_rev (curry Logic.mk_implies) Cs
    17.5        |> fold_rev (Logic.all o Free) ws
    17.6        |> term_conv thy ind_atomize
    17.7 -      |> ObjectLogic.drop_judgment thy
    17.8 +      |> Object_Logic.drop_judgment thy
    17.9        |> tupled_lambda (foldr1 HOLogic.mk_prod (map Free xs))
   17.10    in
   17.11      SumTree.mk_sumcases HOLogic.boolT (map brnch branches)
    18.1 --- a/src/HOL/Tools/Function/termination.ML	Sun Mar 07 11:57:16 2010 +0100
    18.2 +++ b/src/HOL/Tools/Function/termination.ML	Sun Mar 07 12:19:47 2010 +0100
    18.3 @@ -282,7 +282,7 @@
    18.4        let
    18.5          val (vars, prems, lhs, rhs) = dest_term ineq
    18.6        in
    18.7 -        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (ObjectLogic.atomize_term thy) prems)
    18.8 +        mk_pair_compr (fastype_of lhs, vars, lhs, rhs, map (Object_Logic.atomize_term thy) prems)
    18.9        end
   18.10  
   18.11      val relation =
    19.1 --- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Sun Mar 07 11:57:16 2010 +0100
    19.2 +++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Sun Mar 07 12:19:47 2010 +0100
    19.3 @@ -967,10 +967,11 @@
    19.4            (semiring_normalize_wrapper ctxt res)) form));
    19.5  
    19.6  fun ring_tac add_ths del_ths ctxt =
    19.7 -  ObjectLogic.full_atomize_tac
    19.8 -  THEN' asm_full_simp_tac (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths)
    19.9 +  Object_Logic.full_atomize_tac
   19.10 +  THEN' asm_full_simp_tac
   19.11 +    (Simplifier.context ctxt (fst (NormalizerData.get ctxt)) delsimps del_ths addsimps add_ths)
   19.12    THEN' CSUBGOAL (fn (p, i) =>
   19.13 -    rtac (let val form = (ObjectLogic.dest_judgment p)
   19.14 +    rtac (let val form = Object_Logic.dest_judgment p
   19.15            in case get_ring_ideal_convs ctxt form of
   19.16             NONE => reflexive form
   19.17            | SOME thy => #ring_conv thy form
   19.18 @@ -1008,7 +1009,7 @@
   19.19     end
   19.20    in  
   19.21       clarify_tac @{claset} i 
   19.22 -     THEN ObjectLogic.full_atomize_tac i 
   19.23 +     THEN Object_Logic.full_atomize_tac i 
   19.24       THEN asm_full_simp_tac (Simplifier.context ctxt (#poly_eq_ss thy)) i 
   19.25       THEN clarify_tac @{claset} i 
   19.26       THEN (REPEAT (CONVERSION (#unwind_conv thy) i))
    20.1 --- a/src/HOL/Tools/Nitpick/minipick.ML	Sun Mar 07 11:57:16 2010 +0100
    20.2 +++ b/src/HOL/Tools/Nitpick/minipick.ML	Sun Mar 07 12:19:47 2010 +0100
    20.3 @@ -298,7 +298,7 @@
    20.4        | card (Type ("*", [T1, T2])) = card T1 * card T2
    20.5        | card @{typ bool} = 2
    20.6        | card T = Int.max (1, raw_card T)
    20.7 -    val neg_t = @{const Not} $ ObjectLogic.atomize_term thy t
    20.8 +    val neg_t = @{const Not} $ Object_Logic.atomize_term thy t
    20.9      val _ = fold_types (K o check_type ctxt) neg_t ()
   20.10      val frees = Term.add_frees neg_t []
   20.11      val bounds = map2 (bound_for_free card) (index_seq 0 (length frees)) frees
    21.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Mar 07 11:57:16 2010 +0100
    21.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Sun Mar 07 12:19:47 2010 +0100
    21.3 @@ -1762,8 +1762,8 @@
    21.4  (* theory -> styp -> term -> term list * term list * term *)
    21.5  fun triple_for_intro_rule thy x t =
    21.6    let
    21.7 -    val prems = Logic.strip_imp_prems t |> map (ObjectLogic.atomize_term thy)
    21.8 -    val concl = Logic.strip_imp_concl t |> ObjectLogic.atomize_term thy
    21.9 +    val prems = Logic.strip_imp_prems t |> map (Object_Logic.atomize_term thy)
   21.10 +    val concl = Logic.strip_imp_concl t |> Object_Logic.atomize_term thy
   21.11      val (main, side) = List.partition (exists_Const (curry (op =) x)) prems
   21.12      (* term -> bool *)
   21.13       val is_good_head = curry (op =) (Const x) o head_of
    22.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Mar 07 11:57:16 2010 +0100
    22.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Sun Mar 07 12:19:47 2010 +0100
    22.3 @@ -807,7 +807,7 @@
    22.4      fun try_out negate =
    22.5        let
    22.6          val concl = (negate ? curry (op $) @{const Not})
    22.7 -                    (ObjectLogic.atomize_term thy prop)
    22.8 +                    (Object_Logic.atomize_term thy prop)
    22.9          val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
   22.10                     |> map_types (map_type_tfree
   22.11                                       (fn (s, []) => TFree (s, HOLogic.typeS)
    23.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sun Mar 07 11:57:16 2010 +0100
    23.2 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Sun Mar 07 12:19:47 2010 +0100
    23.3 @@ -225,9 +225,9 @@
    23.4    (case dlo_instance ctxt p of
    23.5      NONE => no_tac
    23.6    | SOME instance =>
    23.7 -      ObjectLogic.full_atomize_tac i THEN
    23.8 +      Object_Logic.full_atomize_tac i THEN
    23.9        simp_tac (#simpset (snd instance)) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
   23.10 -      CONVERSION (ObjectLogic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
   23.11 +      CONVERSION (Object_Logic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
   23.12        simp_tac (simpset_of ctxt) i));  (* FIXME really? *)
   23.13  
   23.14  end;
    24.1 --- a/src/HOL/Tools/Qelim/langford.ML	Sun Mar 07 11:57:16 2010 +0100
    24.2 +++ b/src/HOL/Tools/Qelim/langford.ML	Sun Mar 07 12:19:47 2010 +0100
    24.3 @@ -234,11 +234,11 @@
    24.4    (case dlo_instance ctxt p of
    24.5      (ss, NONE) => simp_tac ss i
    24.6    | (ss,  SOME instance) =>
    24.7 -      ObjectLogic.full_atomize_tac i THEN
    24.8 +      Object_Logic.full_atomize_tac i THEN
    24.9        simp_tac ss i
   24.10        THEN (CONVERSION Thm.eta_long_conversion) i
   24.11        THEN (TRY o generalize_tac (cfrees (#atoms instance))) i
   24.12 -      THEN ObjectLogic.full_atomize_tac i
   24.13 -      THEN CONVERSION (ObjectLogic.judgment_conv (raw_dlo_conv ss instance)) i
   24.14 +      THEN Object_Logic.full_atomize_tac i
   24.15 +      THEN CONVERSION (Object_Logic.judgment_conv (raw_dlo_conv ss instance)) i
   24.16        THEN (simp_tac ss i)));  
   24.17  end;
   24.18 \ No newline at end of file
    25.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Sun Mar 07 11:57:16 2010 +0100
    25.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Sun Mar 07 12:19:47 2010 +0100
    25.3 @@ -166,13 +166,13 @@
    25.4      val aprems = Arith_Data.get_arith_facts ctxt
    25.5  in
    25.6    Method.insert_tac aprems
    25.7 -  THEN_ALL_NEW ObjectLogic.full_atomize_tac
    25.8 +  THEN_ALL_NEW Object_Logic.full_atomize_tac
    25.9    THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
   25.10    THEN_ALL_NEW simp_tac ss
   25.11    THEN_ALL_NEW (TRY o generalize_tac (int_nat_terms ctxt))
   25.12 -  THEN_ALL_NEW ObjectLogic.full_atomize_tac
   25.13 +  THEN_ALL_NEW Object_Logic.full_atomize_tac
   25.14    THEN_ALL_NEW (thin_prems_tac (is_relevant ctxt))
   25.15 -  THEN_ALL_NEW ObjectLogic.full_atomize_tac
   25.16 +  THEN_ALL_NEW Object_Logic.full_atomize_tac
   25.17    THEN_ALL_NEW div_mod_tac ctxt
   25.18    THEN_ALL_NEW splits_tac ctxt
   25.19    THEN_ALL_NEW simp_tac ss
    26.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Mar 07 11:57:16 2010 +0100
    26.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sun Mar 07 12:19:47 2010 +0100
    26.3 @@ -48,7 +48,7 @@
    26.4  fun atomize_thm thm =
    26.5  let
    26.6    val thm' = Thm.freezeT (forall_intr_vars thm) (* FIXME/TODO: is this proper Isar-technology? *)
    26.7 -  val thm'' = ObjectLogic.atomize (cprop_of thm')
    26.8 +  val thm'' = Object_Logic.atomize (cprop_of thm')
    26.9  in
   26.10    @{thm equal_elim_rule1} OF [thm'', thm']
   26.11  end
   26.12 @@ -616,7 +616,7 @@
   26.13  
   26.14  (* the tactic leaves three subgoals to be proved *)
   26.15  fun procedure_tac ctxt rthm =
   26.16 -  ObjectLogic.full_atomize_tac
   26.17 +  Object_Logic.full_atomize_tac
   26.18    THEN' gen_frees_tac ctxt
   26.19    THEN' SUBGOAL (fn (goal, i) =>
   26.20      let
    27.1 --- a/src/HOL/Tools/TFL/post.ML	Sun Mar 07 11:57:16 2010 +0100
    27.2 +++ b/src/HOL/Tools/TFL/post.ML	Sun Mar 07 12:19:47 2010 +0100
    27.3 @@ -151,9 +151,9 @@
    27.4                 {f = f, R = R, rules = rules,
    27.5                  full_pats_TCs = full_pats_TCs,
    27.6                  TCs = TCs}
    27.7 -       val rules' = map (Drule.export_without_context o ObjectLogic.rulify_no_asm)
    27.8 +       val rules' = map (Drule.export_without_context o Object_Logic.rulify_no_asm)
    27.9                          (R.CONJUNCTS rules)
   27.10 -         in  {induct = meta_outer (ObjectLogic.rulify_no_asm (induction RS spec')),
   27.11 +         in  {induct = meta_outer (Object_Logic.rulify_no_asm (induction RS spec')),
   27.12          rules = ListPair.zip(rules', rows),
   27.13          tcs = (termination_goals rules') @ tcs}
   27.14     end
   27.15 @@ -180,7 +180,7 @@
   27.16      | solve_eq (th, [a], i) = [(a, i)]
   27.17      | solve_eq (th, splitths as (_ :: _), i) = 
   27.18        (writeln "Proving unsplit equation...";
   27.19 -      [((Drule.export_without_context o ObjectLogic.rulify_no_asm)
   27.20 +      [((Drule.export_without_context o Object_Logic.rulify_no_asm)
   27.21            (CaseSplit.splitto splitths th), i)])
   27.22        (* if there's an error, pretend nothing happened with this definition 
   27.23           We should probably print something out so that the user knows...? *)
    28.1 --- a/src/HOL/Tools/choice_specification.ML	Sun Mar 07 11:57:16 2010 +0100
    28.2 +++ b/src/HOL/Tools/choice_specification.ML	Sun Mar 07 12:19:47 2010 +0100
    28.3 @@ -111,7 +111,7 @@
    28.4            | myfoldr f [] = error "Choice_Specification.process_spec internal error"
    28.5  
    28.6          val rew_imps = alt_props |>
    28.7 -          map (ObjectLogic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
    28.8 +          map (Object_Logic.atomize o Thm.cterm_of thy o Syntax.read_prop_global thy o snd)
    28.9          val props' = rew_imps |>
   28.10            map (HOLogic.dest_Trueprop o term_of o snd o Thm.dest_equals o cprop_of)
   28.11  
    29.1 --- a/src/HOL/Tools/hologic.ML	Sun Mar 07 11:57:16 2010 +0100
    29.2 +++ b/src/HOL/Tools/hologic.ML	Sun Mar 07 12:19:47 2010 +0100
    29.3 @@ -190,14 +190,14 @@
    29.4  
    29.5  fun conj_intr thP thQ =
    29.6    let
    29.7 -    val (P, Q) = pairself (ObjectLogic.dest_judgment o Thm.cprop_of) (thP, thQ)
    29.8 +    val (P, Q) = pairself (Object_Logic.dest_judgment o Thm.cprop_of) (thP, thQ)
    29.9        handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
   29.10      val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
   29.11    in Drule.implies_elim_list (inst @{thm conjI}) [thP, thQ] end;
   29.12  
   29.13  fun conj_elim thPQ =
   29.14    let
   29.15 -    val (P, Q) = Thm.dest_binop (ObjectLogic.dest_judgment (Thm.cprop_of thPQ))
   29.16 +    val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment (Thm.cprop_of thPQ))
   29.17        handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
   29.18      val inst = Thm.instantiate ([], [(@{cpat "?P::bool"}, P), (@{cpat "?Q::bool"}, Q)]);
   29.19      val thP = Thm.implies_elim (inst @{thm conjunct1}) thPQ;
    30.1 --- a/src/HOL/Tools/inductive.ML	Sun Mar 07 11:57:16 2010 +0100
    30.2 +++ b/src/HOL/Tools/inductive.ML	Sun Mar 07 12:19:47 2010 +0100
    30.3 @@ -788,7 +788,7 @@
    30.4         else if coind then
    30.5           singleton (ProofContext.export
    30.6             (snd (Variable.add_fixes (map (fst o dest_Free) params) lthy1)) lthy1)
    30.7 -           (rotate_prems ~1 (ObjectLogic.rulify
    30.8 +           (rotate_prems ~1 (Object_Logic.rulify
    30.9               (fold_rule rec_preds_defs
   30.10                 (rewrite_rule simp_thms'''
   30.11                  (mono RS (fp_def RS @{thm def_coinduct}))))))
    31.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sun Mar 07 11:57:16 2010 +0100
    31.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sun Mar 07 12:19:47 2010 +0100
    31.3 @@ -395,7 +395,7 @@
    31.4            [rtac (#raw_induct ind_info) 1,
    31.5             rewrite_goals_tac rews,
    31.6             REPEAT ((resolve_tac prems THEN_ALL_NEW EVERY'
    31.7 -             [K (rewrite_goals_tac rews), ObjectLogic.atomize_prems_tac,
    31.8 +             [K (rewrite_goals_tac rews), Object_Logic.atomize_prems_tac,
    31.9                DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE]]) 1)]);
   31.10          val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
   31.11            (Long_Name.qualify qualifier "induct" :: vs' @ Ps @ ["correctness"])), thm) thy;
   31.12 @@ -454,7 +454,7 @@
   31.13             etac elimR 1,
   31.14             ALLGOALS (asm_simp_tac HOL_basic_ss),
   31.15             rewrite_goals_tac rews,
   31.16 -           REPEAT ((resolve_tac prems THEN_ALL_NEW (ObjectLogic.atomize_prems_tac THEN'
   31.17 +           REPEAT ((resolve_tac prems THEN_ALL_NEW (Object_Logic.atomize_prems_tac THEN'
   31.18               DEPTH_SOLVE_1 o FIRST' [atac, etac allE, etac impE])) 1)]);
   31.19          val (thm', thy') = PureThy.store_thm (Binding.qualified_name (space_implode "_"
   31.20            (name_of_thm elim :: vs @ Ps @ ["correctness"])), thm) thy
    32.1 --- a/src/HOL/Tools/lin_arith.ML	Sun Mar 07 11:57:16 2010 +0100
    32.2 +++ b/src/HOL/Tools/lin_arith.ML	Sun Mar 07 12:19:47 2010 +0100
    32.3 @@ -901,7 +901,7 @@
    32.4  in
    32.5  
    32.6  fun gen_tac ex ctxt = FIRST' [simple_tac ctxt,
    32.7 -  ObjectLogic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
    32.8 +  Object_Logic.full_atomize_tac THEN' (REPEAT_DETERM o rtac impI) THEN' raw_tac ctxt ex];
    32.9  
   32.10  val tac = gen_tac true;
   32.11  
    33.1 --- a/src/HOL/Tools/meson.ML	Sun Mar 07 11:57:16 2010 +0100
    33.2 +++ b/src/HOL/Tools/meson.ML	Sun Mar 07 12:19:47 2010 +0100
    33.3 @@ -587,7 +587,7 @@
    33.4    Function mkcl converts theorems to clauses.*)
    33.5  fun MESON mkcl cltac ctxt i st =
    33.6    SELECT_GOAL
    33.7 -    (EVERY [ObjectLogic.atomize_prems_tac 1,
    33.8 +    (EVERY [Object_Logic.atomize_prems_tac 1,
    33.9              rtac ccontr 1,
   33.10              Subgoal.FOCUS (fn {context = ctxt', prems = negs, ...} =>
   33.11                        EVERY1 [skolemize_prems_tac ctxt negs,
    34.1 --- a/src/HOL/Tools/record.ML	Sun Mar 07 11:57:16 2010 +0100
    34.2 +++ b/src/HOL/Tools/record.ML	Sun Mar 07 12:19:47 2010 +0100
    34.3 @@ -2214,7 +2214,7 @@
    34.4              [(cterm_of defs_thy Pvar, cterm_of defs_thy
    34.5                (lambda w (HOLogic.imp $ HOLogic.mk_eq (r0, w) $ C)))]
    34.6              induct_scheme;
    34.7 -        in ObjectLogic.rulify (mp OF [ind, refl]) end;
    34.8 +        in Object_Logic.rulify (mp OF [ind, refl]) end;
    34.9  
   34.10      val cases_scheme_prf = future_forward_prf cases_scheme_prf cases_scheme_prop;
   34.11      val cases_scheme = timeit_msg "record cases_scheme proof:" cases_scheme_prf;
    35.1 --- a/src/HOL/Tools/res_axioms.ML	Sun Mar 07 11:57:16 2010 +0100
    35.2 +++ b/src/HOL/Tools/res_axioms.ML	Sun Mar 07 12:19:47 2010 +0100
    35.3 @@ -276,7 +276,7 @@
    35.4    let val th1 = th |> transform_elim |> zero_var_indexes
    35.5        val ((_, [th2]), ctxt) = Variable.import true [th1] ctxt0
    35.6        val th3 = th2
    35.7 -        |> Conv.fconv_rule ObjectLogic.atomize
    35.8 +        |> Conv.fconv_rule Object_Logic.atomize
    35.9          |> Meson.make_nnf ctxt |> strip_lambdas ~1
   35.10    in  (th3, ctxt)  end;
   35.11  
   35.12 @@ -493,7 +493,7 @@
   35.13  (*** Converting a subgoal into negated conjecture clauses. ***)
   35.14  
   35.15  fun neg_skolemize_tac ctxt =
   35.16 -  EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac ctxt];
   35.17 +  EVERY' [rtac ccontr, Object_Logic.atomize_prems_tac, Meson.skolemize_tac ctxt];
   35.18  
   35.19  val neg_clausify = Meson.make_clauses #> map combinators #> Meson.finish_cnf;
   35.20  
    36.1 --- a/src/HOL/Tools/sat_funcs.ML	Sun Mar 07 11:57:16 2010 +0100
    36.2 +++ b/src/HOL/Tools/sat_funcs.ML	Sun Mar 07 12:19:47 2010 +0100
    36.3 @@ -434,7 +434,7 @@
    36.4  
    36.5  val pre_cnf_tac =
    36.6          rtac ccontr THEN'
    36.7 -        ObjectLogic.atomize_prems_tac THEN'
    36.8 +        Object_Logic.atomize_prems_tac THEN'
    36.9          CONVERSION Drule.beta_eta_conversion;
   36.10  
   36.11  (* ------------------------------------------------------------------------- *)
    37.1 --- a/src/HOL/Tools/typedef.ML	Sun Mar 07 11:57:16 2010 +0100
    37.2 +++ b/src/HOL/Tools/typedef.ML	Sun Mar 07 12:19:47 2010 +0100
    37.3 @@ -130,7 +130,7 @@
    37.4            in Drule.export_without_context (Drule.equal_elim_rule2 OF [goal_eq, th]) end;
    37.5  
    37.6      fun typedef_result inhabited =
    37.7 -      ObjectLogic.typedecl (tname, vs, mx)
    37.8 +      Object_Logic.typedecl (tname, vs, mx)
    37.9        #> snd
   37.10        #> Sign.add_consts_i
   37.11          [(Rep_name, newT --> oldT, NoSyn),
    38.1 --- a/src/Provers/blast.ML	Sun Mar 07 11:57:16 2010 +0100
    38.2 +++ b/src/Provers/blast.ML	Sun Mar 07 12:19:47 2010 +0100
    38.3 @@ -181,7 +181,7 @@
    38.4  fun isGoal (Const ("*Goal*", _) $ _) = true
    38.5    | isGoal _ = false;
    38.6  
    38.7 -val TruepropC = ObjectLogic.judgment_name Data.thy;
    38.8 +val TruepropC = Object_Logic.judgment_name Data.thy;
    38.9  val TruepropT = Sign.the_const_type Data.thy TruepropC;
   38.10  
   38.11  fun mk_Trueprop t = Term.$ (Term.Const (TruepropC, TruepropT), t);
   38.12 @@ -1251,7 +1251,7 @@
   38.13  fun timing_depth_tac start cs lim i st0 =
   38.14    let val thy = Thm.theory_of_thm st0
   38.15        val state = initialize thy
   38.16 -      val st = Conv.gconv_rule ObjectLogic.atomize_prems i st0
   38.17 +      val st = Conv.gconv_rule Object_Logic.atomize_prems i st0
   38.18        val skoprem = fromSubgoal thy (List.nth(prems_of st, i-1))
   38.19        val hyps  = strip_imp_prems skoprem
   38.20        and concl = strip_imp_concl skoprem
    39.1 --- a/src/Provers/classical.ML	Sun Mar 07 11:57:16 2010 +0100
    39.2 +++ b/src/Provers/classical.ML	Sun Mar 07 12:19:47 2010 +0100
    39.3 @@ -153,7 +153,7 @@
    39.4  *)
    39.5  
    39.6  fun classical_rule rule =
    39.7 -  if ObjectLogic.is_elim rule then
    39.8 +  if Object_Logic.is_elim rule then
    39.9      let
   39.10        val rule' = rule RS classical;
   39.11        val concl' = Thm.concl_of rule';
   39.12 @@ -173,7 +173,7 @@
   39.13    else rule;
   39.14  
   39.15  (*flatten nested meta connectives in prems*)
   39.16 -val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 ObjectLogic.atomize_prems);
   39.17 +val flat_rule = Conv.fconv_rule (Conv.prems_conv ~1 Object_Logic.atomize_prems);
   39.18  
   39.19  
   39.20  (*** Useful tactics for classical reasoning ***)
   39.21 @@ -724,24 +724,24 @@
   39.22  
   39.23  (*Dumb but fast*)
   39.24  fun fast_tac cs =
   39.25 -  ObjectLogic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   39.26 +  Object_Logic.atomize_prems_tac THEN' SELECT_GOAL (DEPTH_SOLVE (step_tac cs 1));
   39.27  
   39.28  (*Slower but smarter than fast_tac*)
   39.29  fun best_tac cs =
   39.30 -  ObjectLogic.atomize_prems_tac THEN'
   39.31 +  Object_Logic.atomize_prems_tac THEN'
   39.32    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (step_tac cs 1));
   39.33  
   39.34  (*even a bit smarter than best_tac*)
   39.35  fun first_best_tac cs =
   39.36 -  ObjectLogic.atomize_prems_tac THEN'
   39.37 +  Object_Logic.atomize_prems_tac THEN'
   39.38    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (FIRSTGOAL (step_tac cs)));
   39.39  
   39.40  fun slow_tac cs =
   39.41 -  ObjectLogic.atomize_prems_tac THEN'
   39.42 +  Object_Logic.atomize_prems_tac THEN'
   39.43    SELECT_GOAL (DEPTH_SOLVE (slow_step_tac cs 1));
   39.44  
   39.45  fun slow_best_tac cs =
   39.46 -  ObjectLogic.atomize_prems_tac THEN'
   39.47 +  Object_Logic.atomize_prems_tac THEN'
   39.48    SELECT_GOAL (BEST_FIRST (has_fewer_prems 1, sizef) (slow_step_tac cs 1));
   39.49  
   39.50  
   39.51 @@ -749,13 +749,13 @@
   39.52  val weight_ASTAR = Unsynchronized.ref 5;
   39.53  
   39.54  fun astar_tac cs =
   39.55 -  ObjectLogic.atomize_prems_tac THEN'
   39.56 +  Object_Logic.atomize_prems_tac THEN'
   39.57    SELECT_GOAL
   39.58      (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   39.59        (step_tac cs 1));
   39.60  
   39.61  fun slow_astar_tac cs =
   39.62 -  ObjectLogic.atomize_prems_tac THEN'
   39.63 +  Object_Logic.atomize_prems_tac THEN'
   39.64    SELECT_GOAL
   39.65      (ASTAR (has_fewer_prems 1, fn lev => fn thm => size_of_thm thm + !weight_ASTAR * lev)
   39.66        (slow_step_tac cs 1));
    40.1 --- a/src/Provers/splitter.ML	Sun Mar 07 11:57:16 2010 +0100
    40.2 +++ b/src/Provers/splitter.ML	Sun Mar 07 12:19:47 2010 +0100
    40.3 @@ -46,14 +46,14 @@
    40.4  struct
    40.5  
    40.6  val Const (const_not, _) $ _ =
    40.7 -  ObjectLogic.drop_judgment Data.thy
    40.8 +  Object_Logic.drop_judgment Data.thy
    40.9      (#1 (Logic.dest_implies (Thm.prop_of Data.notnotD)));
   40.10  
   40.11  val Const (const_or , _) $ _ $ _ =
   40.12 -  ObjectLogic.drop_judgment Data.thy
   40.13 +  Object_Logic.drop_judgment Data.thy
   40.14      (#1 (Logic.dest_implies (Thm.prop_of Data.disjE)));
   40.15  
   40.16 -val const_Trueprop = ObjectLogic.judgment_name Data.thy;
   40.17 +val const_Trueprop = Object_Logic.judgment_name Data.thy;
   40.18  
   40.19  
   40.20  fun split_format_err () = error "Wrong format for split rule";
    41.1 --- a/src/Pure/Isar/attrib.ML	Sun Mar 07 11:57:16 2010 +0100
    41.2 +++ b/src/Pure/Isar/attrib.ML	Sun Mar 07 12:19:47 2010 +0100
    41.3 @@ -252,7 +252,7 @@
    41.4  (* rule format *)
    41.5  
    41.6  val rule_format = Args.mode "no_asm"
    41.7 -  >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format);
    41.8 +  >> (fn true => Object_Logic.rule_format_no_asm | false => Object_Logic.rule_format);
    41.9  
   41.10  val elim_format = Thm.rule_attribute (K Tactic.make_elim);
   41.11  
   41.12 @@ -306,9 +306,9 @@
   41.13    setup (Binding.name "no_vars") (Scan.succeed no_vars) "frozen schematic vars" #>
   41.14    setup (Binding.name "eta_long") (Scan.succeed eta_long)
   41.15      "put theorem into eta long beta normal form" #>
   41.16 -  setup (Binding.name "atomize") (Scan.succeed ObjectLogic.declare_atomize)
   41.17 +  setup (Binding.name "atomize") (Scan.succeed Object_Logic.declare_atomize)
   41.18      "declaration of atomize rule" #>
   41.19 -  setup (Binding.name "rulify") (Scan.succeed ObjectLogic.declare_rulify)
   41.20 +  setup (Binding.name "rulify") (Scan.succeed Object_Logic.declare_rulify)
   41.21      "declaration of rulify rule" #>
   41.22    setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
   41.23    setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
    42.1 --- a/src/Pure/Isar/auto_bind.ML	Sun Mar 07 11:57:16 2010 +0100
    42.2 +++ b/src/Pure/Isar/auto_bind.ML	Sun Mar 07 12:19:47 2010 +0100
    42.3 @@ -23,7 +23,7 @@
    42.4  val thisN = "this";
    42.5  val assmsN = "assms";
    42.6  
    42.7 -fun strip_judgment thy = ObjectLogic.drop_judgment thy o Logic.strip_assums_concl;
    42.8 +fun strip_judgment thy = Object_Logic.drop_judgment thy o Logic.strip_assums_concl;
    42.9  
   42.10  fun statement_binds thy name prop =
   42.11    [((name, 0), SOME (Term.list_abs (Logic.strip_params prop, strip_judgment thy prop)))];
    43.1 --- a/src/Pure/Isar/element.ML	Sun Mar 07 11:57:16 2010 +0100
    43.2 +++ b/src/Pure/Isar/element.ML	Sun Mar 07 12:19:47 2010 +0100
    43.3 @@ -223,12 +223,12 @@
    43.4      val cert = Thm.cterm_of thy;
    43.5  
    43.6      val th = MetaSimplifier.norm_hhf raw_th;
    43.7 -    val is_elim = ObjectLogic.is_elim th;
    43.8 +    val is_elim = Object_Logic.is_elim th;
    43.9  
   43.10      val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body false ctxt);
   43.11      val prop = Thm.prop_of th';
   43.12      val (prems, concl) = Logic.strip_horn prop;
   43.13 -    val concl_term = ObjectLogic.drop_judgment thy concl;
   43.14 +    val concl_term = Object_Logic.drop_judgment thy concl;
   43.15  
   43.16      val fixes = fold_aterms (fn v as Free (x, T) =>
   43.17          if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
    44.1 --- a/src/Pure/Isar/expression.ML	Sun Mar 07 11:57:16 2010 +0100
    44.2 +++ b/src/Pure/Isar/expression.ML	Sun Mar 07 12:19:47 2010 +0100
    44.3 @@ -595,11 +595,11 @@
    44.4  fun atomize_spec thy ts =
    44.5    let
    44.6      val t = Logic.mk_conjunction_balanced ts;
    44.7 -    val body = ObjectLogic.atomize_term thy t;
    44.8 +    val body = Object_Logic.atomize_term thy t;
    44.9      val bodyT = Term.fastype_of body;
   44.10    in
   44.11      if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t))
   44.12 -    else (body, bodyT, ObjectLogic.atomize (Thm.cterm_of thy t))
   44.13 +    else (body, bodyT, Object_Logic.atomize (Thm.cterm_of thy t))
   44.14    end;
   44.15  
   44.16  (* achieve plain syntax for locale predicates (without "PROP") *)
   44.17 @@ -634,7 +634,7 @@
   44.18  
   44.19      val args = map Logic.mk_type extraTs @ map Free xs;
   44.20      val head = Term.list_comb (Const (name, predT), args);
   44.21 -    val statement = ObjectLogic.ensure_propT thy head;
   44.22 +    val statement = Object_Logic.ensure_propT thy head;
   44.23  
   44.24      val ([pred_def], defs_thy) =
   44.25        thy
    45.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Mar 07 11:57:16 2010 +0100
    45.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Mar 07 12:19:47 2010 +0100
    45.3 @@ -105,7 +105,7 @@
    45.4  val _ =
    45.5    OuterSyntax.command "typedecl" "type declaration" K.thy_decl
    45.6      (P.type_args -- P.binding -- P.opt_mixfix >> (fn ((args, a), mx) =>
    45.7 -      Toplevel.theory (ObjectLogic.typedecl (a, args, mx) #> snd)));
    45.8 +      Toplevel.theory (Object_Logic.typedecl (a, args, mx) #> snd)));
    45.9  
   45.10  val _ =
   45.11    OuterSyntax.command "types" "declare type abbreviations" K.thy_decl
   45.12 @@ -127,7 +127,7 @@
   45.13  
   45.14  val _ =
   45.15    OuterSyntax.command "judgment" "declare object-logic judgment" K.thy_decl
   45.16 -    (P.const_binding >> (Toplevel.theory o ObjectLogic.add_judgment_cmd));
   45.17 +    (P.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
   45.18  
   45.19  val _ =
   45.20    OuterSyntax.command "consts" "declare constants" K.thy_decl
    46.1 --- a/src/Pure/Isar/method.ML	Sun Mar 07 11:57:16 2010 +0100
    46.2 +++ b/src/Pure/Isar/method.ML	Sun Mar 07 12:19:47 2010 +0100
    46.3 @@ -171,8 +171,8 @@
    46.4  
    46.5  (* atomize rule statements *)
    46.6  
    46.7 -fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o ObjectLogic.atomize_prems_tac)
    46.8 -  | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o ObjectLogic.full_atomize_tac)));
    46.9 +fun atomize false = SIMPLE_METHOD' (CHANGED_PROP o Object_Logic.atomize_prems_tac)
   46.10 +  | atomize true = RAW_METHOD (K (HEADGOAL (CHANGED_PROP o Object_Logic.full_atomize_tac)));
   46.11  
   46.12  
   46.13  (* this -- resolve facts directly *)
    47.1 --- a/src/Pure/Isar/object_logic.ML	Sun Mar 07 11:57:16 2010 +0100
    47.2 +++ b/src/Pure/Isar/object_logic.ML	Sun Mar 07 12:19:47 2010 +0100
    47.3 @@ -34,7 +34,7 @@
    47.4    val rule_format_no_asm: attribute
    47.5  end;
    47.6  
    47.7 -structure ObjectLogic: OBJECT_LOGIC =
    47.8 +structure Object_Logic: OBJECT_LOGIC =
    47.9  struct
   47.10  
   47.11  (** theory data **)
    48.1 --- a/src/Pure/Isar/obtain.ML	Sun Mar 07 11:57:16 2010 +0100
    48.2 +++ b/src/Pure/Isar/obtain.ML	Sun Mar 07 12:19:47 2010 +0100
    48.3 @@ -76,7 +76,7 @@
    48.4      val thy = ProofContext.theory_of fix_ctxt;
    48.5  
    48.6      val _ = eliminate_term fix_ctxt xs (Thm.full_prop_of thm);
    48.7 -    val _ = ObjectLogic.is_judgment thy (Thm.concl_of thm) orelse
    48.8 +    val _ = Object_Logic.is_judgment thy (Thm.concl_of thm) orelse
    48.9        error "Conclusion in obtained context must be object-logic judgment";
   48.10  
   48.11      val ((_, [thm']), ctxt') = Variable.import true [thm] fix_ctxt;
   48.12 @@ -100,7 +100,7 @@
   48.13  fun bind_judgment ctxt name =
   48.14    let
   48.15      val (bind, ctxt') = ProofContext.bind_fixes [name] ctxt;
   48.16 -    val (t as _ $ Free v) = bind (ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) name);
   48.17 +    val (t as _ $ Free v) = bind (Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) name);
   48.18    in ((v, t), ctxt') end;
   48.19  
   48.20  val thatN = "that";
    49.1 --- a/src/Pure/Isar/rule_cases.ML	Sun Mar 07 11:57:16 2010 +0100
    49.2 +++ b/src/Pure/Isar/rule_cases.ML	Sun Mar 07 12:19:47 2010 +0100
    49.3 @@ -110,7 +110,7 @@
    49.4          val (assumes1, assumes2) = extract_assumes (Long_Name.qualify name) case_outline prop
    49.5            |> pairself (map (apsnd (maps Logic.dest_conjunctions)));
    49.6  
    49.7 -        val concl = ObjectLogic.drop_judgment thy (Logic.strip_assums_concl prop);
    49.8 +        val concl = Object_Logic.drop_judgment thy (Logic.strip_assums_concl prop);
    49.9          val binds =
   49.10            (case_conclN, concl) :: dest_binops concls concl
   49.11            |> map (fn (x, t) => ((x, 0), SOME (abs_fixes t)));
    50.1 --- a/src/Pure/Isar/specification.ML	Sun Mar 07 11:57:16 2010 +0100
    50.2 +++ b/src/Pure/Isar/specification.ML	Sun Mar 07 12:19:47 2010 +0100
    50.3 @@ -316,7 +316,7 @@
    50.4          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
    50.5          val (propp, elems_ctxt) = prep_stmt (elems @ constraints) raw_propp ctxt;
    50.6  
    50.7 -        val thesis = ObjectLogic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
    50.8 +        val thesis = Object_Logic.fixed_judgment (ProofContext.theory_of ctxt) Auto_Bind.thesisN;
    50.9  
   50.10          fun assume_case ((name, (vars, _)), asms) ctxt' =
   50.11            let
    51.1 --- a/src/Pure/Thy/term_style.ML	Sun Mar 07 11:57:16 2010 +0100
    51.2 +++ b/src/Pure/Thy/term_style.ML	Sun Mar 07 12:19:47 2010 +0100
    51.3 @@ -64,8 +64,8 @@
    51.4  
    51.5  fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t =>
    51.6    let
    51.7 -    val concl = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt)
    51.8 -      (Logic.strip_imp_concl t)
    51.9 +    val concl =
   51.10 +      Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t)
   51.11    in
   51.12      case concl of (_ $ l $ r) => proj (l, r)
   51.13      | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
    52.1 --- a/src/Pure/Tools/find_theorems.ML	Sun Mar 07 11:57:16 2010 +0100
    52.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Mar 07 12:19:47 2010 +0100
    52.3 @@ -93,7 +93,7 @@
    52.4  
    52.5  (* matching theorems *)
    52.6  
    52.7 -fun is_nontrivial thy = Term.is_Const o Term.head_of o ObjectLogic.drop_judgment thy;
    52.8 +fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
    52.9  
   52.10  (*educated guesses on HOL*)  (* FIXME broken *)
   52.11  val boolT = Type ("bool", []);
   52.12 @@ -110,13 +110,13 @@
   52.13      fun check_match pat = Pattern.matches thy (if po then (pat, obj) else (obj, pat));
   52.14      fun matches pat =
   52.15        let
   52.16 -        val jpat = ObjectLogic.drop_judgment thy pat;
   52.17 +        val jpat = Object_Logic.drop_judgment thy pat;
   52.18          val c = Term.head_of jpat;
   52.19          val pats =
   52.20            if Term.is_Const c
   52.21            then
   52.22              if doiff andalso c = iff_const then
   52.23 -              (pat :: map (ObjectLogic.ensure_propT thy) (snd (strip_comb jpat)))
   52.24 +              (pat :: map (Object_Logic.ensure_propT thy) (snd (strip_comb jpat)))
   52.25                  |> filter (is_nontrivial thy)
   52.26              else [pat]
   52.27            else [];
    53.1 --- a/src/Pure/old_goals.ML	Sun Mar 07 11:57:16 2010 +0100
    53.2 +++ b/src/Pure/old_goals.ML	Sun Mar 07 12:19:47 2010 +0100
    53.3 @@ -606,11 +606,11 @@
    53.4  fun qed_goalw name thy rews goal tacsf =
    53.5    ML_Context.ml_store_thm (name, prove_goalw thy rews goal tacsf);
    53.6  fun qed_spec_mp name =
    53.7 -  ML_Context.ml_store_thm (name, ObjectLogic.rulify_no_asm (result ()));
    53.8 +  ML_Context.ml_store_thm (name, Object_Logic.rulify_no_asm (result ()));
    53.9  fun qed_goal_spec_mp name thy s p =
   53.10 -  bind_thm (name, ObjectLogic.rulify_no_asm (prove_goal thy s p));
   53.11 +  bind_thm (name, Object_Logic.rulify_no_asm (prove_goal thy s p));
   53.12  fun qed_goalw_spec_mp name thy defs s p =
   53.13 -  bind_thm (name, ObjectLogic.rulify_no_asm (prove_goalw thy defs s p));
   53.14 +  bind_thm (name, Object_Logic.rulify_no_asm (prove_goalw thy defs s p));
   53.15  
   53.16  end;
   53.17  
    54.1 --- a/src/Tools/atomize_elim.ML	Sun Mar 07 11:57:16 2010 +0100
    54.2 +++ b/src/Tools/atomize_elim.ML	Sun Mar 07 12:19:47 2010 +0100
    54.3 @@ -59,9 +59,9 @@
    54.4     (EX x y z. ...) | ... | (EX a b c. ...)
    54.5  *)
    54.6  fun atomize_elim_conv ctxt ct =
    54.7 -    (forall_conv (K (prems_conv ~1 ObjectLogic.atomize_prems)) ctxt
    54.8 +    (forall_conv (K (prems_conv ~1 Object_Logic.atomize_prems)) ctxt
    54.9      then_conv MetaSimplifier.rewrite true (AtomizeElimData.get ctxt)
   54.10 -    then_conv (fn ct' => if can ObjectLogic.dest_judgment ct'
   54.11 +    then_conv (fn ct' => if can Object_Logic.dest_judgment ct'
   54.12                           then all_conv ct'
   54.13                           else raise CTERM ("atomize_elim", [ct', ct])))
   54.14      ct
    55.1 --- a/src/Tools/induct.ML	Sun Mar 07 11:57:16 2010 +0100
    55.2 +++ b/src/Tools/induct.ML	Sun Mar 07 12:19:47 2010 +0100
    55.3 @@ -137,7 +137,7 @@
    55.4        Conv.implies_concl_conv (swap_prems_conv (i-1)) then_conv
    55.5        Conv.rewr_conv Drule.swap_prems_eq
    55.6  
    55.7 -fun drop_judgment ctxt = ObjectLogic.drop_judgment (ProofContext.theory_of ctxt);
    55.8 +fun drop_judgment ctxt = Object_Logic.drop_judgment (ProofContext.theory_of ctxt);
    55.9  
   55.10  fun find_eq ctxt t =
   55.11    let
   55.12 @@ -511,7 +511,7 @@
   55.13  
   55.14  fun atomize_term thy =
   55.15    MetaSimplifier.rewrite_term thy Data.atomize []
   55.16 -  #> ObjectLogic.drop_judgment thy;
   55.17 +  #> Object_Logic.drop_judgment thy;
   55.18  
   55.19  val atomize_cterm = MetaSimplifier.rewrite true Data.atomize;
   55.20  
    56.1 --- a/src/Tools/induct_tacs.ML	Sun Mar 07 11:57:16 2010 +0100
    56.2 +++ b/src/Tools/induct_tacs.ML	Sun Mar 07 12:19:47 2010 +0100
    56.3 @@ -92,7 +92,7 @@
    56.4              (_, rule) :: _ => rule
    56.5            | [] => raise THM ("No induction rules", 0, [])));
    56.6  
    56.7 -    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 ObjectLogic.atomize);
    56.8 +    val rule' = rule |> Conv.fconv_rule (Conv.concl_conv ~1 Object_Logic.atomize);
    56.9      val _ = Method.trace ctxt [rule'];
   56.10  
   56.11      val concls = Logic.dest_conjunctions (Thm.concl_of rule);
    57.1 --- a/src/Tools/intuitionistic.ML	Sun Mar 07 11:57:16 2010 +0100
    57.2 +++ b/src/Tools/intuitionistic.ML	Sun Mar 07 12:19:47 2010 +0100
    57.3 @@ -89,7 +89,7 @@
    57.4    Method.setup name
    57.5      (Scan.lift (Scan.option OuterParse.nat) --| Method.sections modifiers >>
    57.6        (fn opt_lim => fn ctxt =>
    57.7 -        SIMPLE_METHOD' (ObjectLogic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
    57.8 +        SIMPLE_METHOD' (Object_Logic.atomize_prems_tac THEN' prover_tac ctxt opt_lim)))
    57.9      "intuitionistic proof search";
   57.10  
   57.11  end;
    58.1 --- a/src/Tools/quickcheck.ML	Sun Mar 07 11:57:16 2010 +0100
    58.2 +++ b/src/Tools/quickcheck.ML	Sun Mar 07 12:19:47 2010 +0100
    58.3 @@ -199,7 +199,7 @@
    58.4      val gi' = Logic.list_implies (if no_assms then [] else assms,
    58.5                                    subst_bounds (frees, strip gi))
    58.6        |> monomorphic_term thy insts default_T
    58.7 -      |> ObjectLogic.atomize_term thy;
    58.8 +      |> Object_Logic.atomize_term thy;
    58.9    in gen_test_term ctxt quiet report generator_name size iterations gi' end;
   58.10  
   58.11  fun pretty_counterex ctxt NONE = Pretty.str "Quickcheck found no counterexample."