# HG changeset patch
# User wenzelm
# Date 1229011486 -3600
# Node ID d53f78cafb868c1e9bf8c38a3025be22b7b8caa8
# Parent  7619f0561cd7d7ab17d35423170ac2a0beac4043# Parent  70a61d58460e6cd199ad7543e33575553dddc671
merged

diff -r 7619f0561cd7 -r d53f78cafb86 src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -361,7 +361,7 @@
                 | NONE => fn i => no_tac)
 
 fun distinct_simproc names =
-  Simplifier.simproc HOL.thy "DistinctTreeProver.distinct_simproc" ["x = y"]
+  Simplifier.simproc @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]
     (fn thy => fn ss => fn (Const ("op =",_)$x$y) =>
         case #context (#1 (rep_ss ss)) of
         SOME ctxt => Option.map (fn neq => neq_to_eq_False OF [neq]) 
diff -r 7619f0561cd7 -r d53f78cafb86 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -49,7 +49,7 @@
 
 in
 val lazy_conj_simproc =
-  Simplifier.simproc HOL.thy "lazy_conj_simp" ["P & Q"]
+  Simplifier.simproc @{theory HOL} "lazy_conj_simp" ["P & Q"]
     (fn thy => fn ss => fn t =>
       (case t of (Const ("op &",_)$P$Q) => 
          let
@@ -273,7 +273,7 @@
      end;
 in
 val ex_lookup_eq_simproc =
-  Simplifier.simproc HOL.thy "ex_lookup_eq_simproc" ["Ex t"]
+  Simplifier.simproc @{theory HOL} "ex_lookup_eq_simproc" ["Ex t"]
     (fn thy => fn ss => fn t =>
        let
          val ctxt = Simplifier.the_context ss |>
diff -r 7619f0561cd7 -r d53f78cafb86 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Statespace/state_space.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -230,7 +230,7 @@
                 | NONE => fn i => no_tac)
 
 val distinct_simproc =
-  Simplifier.simproc HOL.thy "StateSpace.distinct_simproc" ["x = y"]
+  Simplifier.simproc @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
     (fn thy => fn ss => (fn (Const ("op =",_)$(x as Free _)$(y as Free _)) =>
         (case #context (#1 (rep_ss ss)) of
           SOME ctxt => Option.map (fn neq => DistinctTreeProver.neq_to_eq_False OF [neq])
diff -r 7619f0561cd7 -r d53f78cafb86 src/HOL/Tools/TFL/dcterm.ML
--- a/src/HOL/Tools/TFL/dcterm.ML	Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/TFL/dcterm.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -74,7 +74,7 @@
  * Some simple constructor functions.
  *---------------------------------------------------------------------------*)
 
-val mk_hol_const = Thm.cterm_of HOL.thy o Const;
+val mk_hol_const = Thm.cterm_of @{theory HOL} o Const;
 
 fun mk_exists (r as (Bvar, Body)) =
   let val ty = #T(rep_cterm Bvar)
diff -r 7619f0561cd7 -r d53f78cafb86 src/HOL/Tools/TFL/post.ML
--- a/src/HOL/Tools/TFL/post.ML	Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/TFL/post.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -81,7 +81,7 @@
    handle U.ERR _ => false;
    
 
-fun prover s = prove_goal HOL.thy s (fn _ => [fast_tac HOL_cs 1]);
+fun prover s = prove_goal @{theory HOL} s (fn _ => [fast_tac HOL_cs 1]);
 val P_imp_P_iff_True = prover "P --> (P= True)" RS mp;
 val P_imp_P_eq_True = P_imp_P_iff_True RS eq_reflection;
 fun mk_meta_eq r = case concl_of r of
diff -r 7619f0561cd7 -r d53f78cafb86 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -275,7 +275,7 @@
   | distinct_proc _ _ _ = NONE;
 
 val distinct_simproc =
-  Simplifier.simproc HOL.thy distinctN ["s = t"] distinct_proc;
+  Simplifier.simproc @{theory HOL} distinctN ["s = t"] distinct_proc;
 
 val dist_ss = HOL_ss addsimprocs [distinct_simproc];
 
diff -r 7619f0561cd7 -r d53f78cafb86 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -97,7 +97,7 @@
 val notTrueE = TrueI RSN (2, notE);
 val notFalseI = Seq.hd (atac 1 notI);
 val simp_thms' = map (fn s => mk_meta_eq (the (find_first
-  (equal (OldGoals.read_prop HOL.thy s) o prop_of) simp_thms)))
+  (equal (OldGoals.read_prop @{theory HOL} s) o prop_of) simp_thms)))
   ["(~True) = False", "(~False) = True",
    "(True --> ?P) = ?P", "(False --> ?P) = True",
    "(?P & True) = ?P", "(True & ?P) = ?P"];
@@ -410,7 +410,7 @@
 local
 
 (*delete needless equality assumptions*)
-val refl_thin = Goal.prove_global HOL.thy [] [] @{prop "!!P. a = a ==> P ==> P"}
+val refl_thin = Goal.prove_global @{theory HOL} [] [] @{prop "!!P. a = a ==> P ==> P"}
   (fn _ => assume_tac 1);
 val elim_rls = [asm_rl, FalseE, refl_thin, conjE, exE];
 val elim_tac = REPEAT o Tactic.eresolve_tac elim_rls;
diff -r 7619f0561cd7 -r d53f78cafb86 src/HOL/Tools/inductive_set_package.ML
--- a/src/HOL/Tools/inductive_set_package.ML	Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -66,7 +66,7 @@
 val anyt = Free ("t", TFree ("'t", []));
 
 fun strong_ind_simproc tab =
-  Simplifier.simproc_i HOL.thy "strong_ind" [anyt] (fn thy => fn ss => fn t =>
+  Simplifier.simproc_i @{theory HOL} "strong_ind" [anyt] (fn thy => fn ss => fn t =>
     let
       fun close p t f =
         let val vs = Term.add_vars t []
@@ -317,7 +317,7 @@
 fun to_pred_simproc rules =
   let val rules' = map mk_meta_eq rules
   in
-    Simplifier.simproc_i HOL.thy "to_pred" [anyt]
+    Simplifier.simproc_i @{theory HOL} "to_pred" [anyt]
       (fn thy => K (lookup_rule thy (prop_of #> Logic.dest_equals) rules'))
   end;
 
diff -r 7619f0561cd7 -r d53f78cafb86 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/record_package.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -858,7 +858,7 @@
   if !record_quick_and_dirty_sensitive andalso !quick_and_dirty
   then Goal.prove (ProofContext.init thy) [] []
         (Logic.list_implies (map Logic.varify asms,Logic.varify prop))
-        (K (SkipProof.cheat_tac HOL.thy))
+        (K (SkipProof.cheat_tac @{theory HOL}))
         (* standard can take quite a while for large records, thats why
          * we varify the proposition manually here.*)
   else let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac;
@@ -924,7 +924,7 @@
  * usual split rules for extensions can apply.
  *)
 val record_split_f_more_simproc =
-  Simplifier.simproc HOL.thy "record_split_f_more_simp" ["x"]
+  Simplifier.simproc @{theory HOL} "record_split_f_more_simp" ["x"]
     (fn thy => fn _ => fn t =>
       (case t of (Const ("all", Type (_, [Type (_, [Type("fun",[T,T']), _]), _])))$
                   (trm as Abs _) =>
@@ -1000,7 +1000,7 @@
  *   subrecord.
  *)
 val record_simproc =
-  Simplifier.simproc HOL.thy "record_simp" ["x"]
+  Simplifier.simproc @{theory HOL} "record_simp" ["x"]
     (fn thy => fn ss => fn t =>
       (case t of (sel as Const (s, Type (_,[domS,rangeS])))$
                    ((upd as Const (u,Type(_,[_,Type (_,[rT,_])]))) $ k $ r)=>
@@ -1063,7 +1063,7 @@
  * (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|)
 *)
 val record_upd_simproc =
-  Simplifier.simproc HOL.thy "record_upd_simp" ["x"]
+  Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
     (fn thy => fn ss => fn t =>
       (case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) =>
          let datatype ('a,'b) calc = Init of 'b | Inter of 'a
@@ -1202,7 +1202,7 @@
  *
  *)
 val record_eq_simproc =
-  Simplifier.simproc HOL.thy "record_eq_simp" ["r = s"]
+  Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"]
     (fn thy => fn _ => fn t =>
       (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
         (case rec_id (~1) T of
@@ -1220,7 +1220,7 @@
  * P t > 0: split up to given bound of record extensions
  *)
 fun record_split_simproc P =
-  Simplifier.simproc HOL.thy "record_split_simp" ["x"]
+  Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
     (fn thy => fn _ => fn t =>
       (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm =>
          if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex"
@@ -1243,7 +1243,7 @@
        | _ => NONE))
 
 val record_ex_sel_eq_simproc =
-  Simplifier.simproc HOL.thy "record_ex_sel_eq_simproc" ["Ex t"]
+  Simplifier.simproc @{theory HOL} "record_ex_sel_eq_simproc" ["Ex t"]
     (fn thy => fn ss => fn t =>
        let
          fun prove prop =
diff -r 7619f0561cd7 -r d53f78cafb86 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -38,8 +38,8 @@
 
 (**** Transformation of Elimination Rules into First-Order Formulas****)
 
-val cfalse = cterm_of HOL.thy HOLogic.false_const;
-val ctp_false = cterm_of HOL.thy (HOLogic.mk_Trueprop HOLogic.false_const);
+val cfalse = cterm_of @{theory HOL} HOLogic.false_const;
+val ctp_false = cterm_of @{theory HOL} (HOLogic.mk_Trueprop HOLogic.false_const);
 
 (*Converts an elim-rule into an equivalent theorem that does not have the
   predicate variable.  Leaves other theorems unchanged.  We simply instantiate the
@@ -47,9 +47,9 @@
 fun transform_elim th =
   case concl_of th of    (*conclusion variable*)
        Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) =>
-           Thm.instantiate ([], [(cterm_of HOL.thy v, cfalse)]) th
+           Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
     | v as Var(_, Type("prop",[])) =>
-           Thm.instantiate ([], [(cterm_of HOL.thy v, ctp_false)]) th
+           Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
     | _ => th;
 
 (*To enforce single-threading*)
@@ -236,7 +236,7 @@
        TrueI);  (*A type variable of sort {} will cause make abstraction fail.*)
 
 (*cterms are used throughout for efficiency*)
-val cTrueprop = Thm.cterm_of HOL.thy HOLogic.Trueprop;
+val cTrueprop = Thm.cterm_of @{theory HOL} HOLogic.Trueprop;
 
 (*cterm version of mk_cTrueprop*)
 fun c_mkTrueprop A = Thm.capply cTrueprop A;
diff -r 7619f0561cd7 -r d53f78cafb86 src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Dec 11 16:50:18 2008 +0100
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Thu Dec 11 17:04:46 2008 +0100
@@ -106,15 +106,9 @@
 
 (* ----- general proofs ----------------------------------------------------- *)
 
-val all2E = prove_goal HOL.thy "[| !x y . P x y; P x y ==> R |] ==> R"
-  (fn prems =>[
-    resolve_tac prems 1,
-    cut_facts_tac prems 1,
-    fast_tac HOL_cs 1]);
+val all2E = @{lemma "!x y . P x y ==> (P x y ==> R) ==> R" by simp}
 
-val dist_eqI = prove_goal (the_context ()) "!!x::'a::po. ~ x << y ==> x ~= y" 
-  (fn prems =>
-    [blast_tac (@{claset} addDs [antisym_less_inverse]) 1]);
+val dist_eqI = @{lemma "!!x::'a::po. ~ x << y ==> x ~= y" by (blast dest!: antisym_less_inverse)}
 
 in