src/HOL/Tools/record_package.ML
changeset 29064 70a61d58460e
parent 29004 a5a91f387791
child 29265 5b4247055bd7
     1.1 --- a/src/HOL/Tools/record_package.ML	Wed Dec 10 06:34:10 2008 -0800
     1.2 +++ b/src/HOL/Tools/record_package.ML	Wed Dec 10 22:55:15 2008 +0100
     1.3 @@ -858,7 +858,7 @@
     1.4    if !record_quick_and_dirty_sensitive andalso !quick_and_dirty
     1.5    then Goal.prove (ProofContext.init thy) [] []
     1.6          (Logic.list_implies (map Logic.varify asms,Logic.varify prop))
     1.7 -        (K (SkipProof.cheat_tac HOL.thy))
     1.8 +        (K (SkipProof.cheat_tac @{theory HOL}))
     1.9          (* standard can take quite a while for large records, thats why
    1.10           * we varify the proposition manually here.*)
    1.11    else let val prf = Goal.prove (ProofContext.init thy) [] asms prop tac;
    1.12 @@ -924,7 +924,7 @@
    1.13   * usual split rules for extensions can apply.
    1.14   *)
    1.15  val record_split_f_more_simproc =
    1.16 -  Simplifier.simproc HOL.thy "record_split_f_more_simp" ["x"]
    1.17 +  Simplifier.simproc @{theory HOL} "record_split_f_more_simp" ["x"]
    1.18      (fn thy => fn _ => fn t =>
    1.19        (case t of (Const ("all", Type (_, [Type (_, [Type("fun",[T,T']), _]), _])))$
    1.20                    (trm as Abs _) =>
    1.21 @@ -1000,7 +1000,7 @@
    1.22   *   subrecord.
    1.23   *)
    1.24  val record_simproc =
    1.25 -  Simplifier.simproc HOL.thy "record_simp" ["x"]
    1.26 +  Simplifier.simproc @{theory HOL} "record_simp" ["x"]
    1.27      (fn thy => fn ss => fn t =>
    1.28        (case t of (sel as Const (s, Type (_,[domS,rangeS])))$
    1.29                     ((upd as Const (u,Type(_,[_,Type (_,[rT,_])]))) $ k $ r)=>
    1.30 @@ -1063,7 +1063,7 @@
    1.31   * (But r(|more := r; A := A (r(|more := r|))|) = r(|more := r|)
    1.32  *)
    1.33  val record_upd_simproc =
    1.34 -  Simplifier.simproc HOL.thy "record_upd_simp" ["x"]
    1.35 +  Simplifier.simproc @{theory HOL} "record_upd_simp" ["x"]
    1.36      (fn thy => fn ss => fn t =>
    1.37        (case t of ((upd as Const (u, Type(_,[_,Type(_,[rT,_])]))) $ k $ r) =>
    1.38           let datatype ('a,'b) calc = Init of 'b | Inter of 'a
    1.39 @@ -1202,7 +1202,7 @@
    1.40   *
    1.41   *)
    1.42  val record_eq_simproc =
    1.43 -  Simplifier.simproc HOL.thy "record_eq_simp" ["r = s"]
    1.44 +  Simplifier.simproc @{theory HOL} "record_eq_simp" ["r = s"]
    1.45      (fn thy => fn _ => fn t =>
    1.46        (case t of Const ("op =", Type (_, [T, _])) $ _ $ _ =>
    1.47          (case rec_id (~1) T of
    1.48 @@ -1220,7 +1220,7 @@
    1.49   * P t > 0: split up to given bound of record extensions
    1.50   *)
    1.51  fun record_split_simproc P =
    1.52 -  Simplifier.simproc HOL.thy "record_split_simp" ["x"]
    1.53 +  Simplifier.simproc @{theory HOL} "record_split_simp" ["x"]
    1.54      (fn thy => fn _ => fn t =>
    1.55        (case t of (Const (quantifier, Type (_, [Type (_, [T, _]), _])))$trm =>
    1.56           if quantifier = "All" orelse quantifier = "all" orelse quantifier = "Ex"
    1.57 @@ -1243,7 +1243,7 @@
    1.58         | _ => NONE))
    1.59  
    1.60  val record_ex_sel_eq_simproc =
    1.61 -  Simplifier.simproc HOL.thy "record_ex_sel_eq_simproc" ["Ex t"]
    1.62 +  Simplifier.simproc @{theory HOL} "record_ex_sel_eq_simproc" ["Ex t"]
    1.63      (fn thy => fn ss => fn t =>
    1.64         let
    1.65           fun prove prop =