ML antiquotes;
authorwenzelm
Wed Apr 04 00:10:59 2007 +0200 (2007-04-04)
changeset 225771a08fce38565
parent 22576 1beba4e2aa9f
child 22578 b0eb5652f210
ML antiquotes;
src/FOLP/FOLP.thy
src/HOL/Fun.thy
src/HOL/Product_Type.thy
src/HOLCF/Pcpo.thy
     1.1 --- a/src/FOLP/FOLP.thy	Tue Apr 03 19:31:48 2007 +0200
     1.2 +++ b/src/FOLP/FOLP.thy	Wed Apr 04 00:10:59 2007 +0200
     1.3 @@ -38,15 +38,14 @@
     1.4    val imp_intr = impI
     1.5  
     1.6    (*etac rev_cut_eq moves an equality to be the last premise. *)
     1.7 -  val rev_cut_eq = prove_goal (the_context ())
     1.8 +  val rev_cut_eq = prove_goal @{theory}
     1.9                  "[| p:a=b;  !!x. x:a=b ==> f(x):R |] ==> ?p:R"
    1.10     (fn prems => [ REPEAT(resolve_tac prems 1) ]);
    1.11  
    1.12    val rev_mp = rev_mp
    1.13    val subst = subst
    1.14    val sym = sym
    1.15 -  val thin_refl = prove_goal (the_context ())
    1.16 -                  "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
    1.17 +  val thin_refl = prove_goal @{theory} "!!X. [|p:x=x; PROP W|] ==> PROP W" (K [atac 1]);
    1.18    end;
    1.19  
    1.20  structure Hypsubst = HypsubstFun(Hypsubst_Data);
     2.1 --- a/src/HOL/Fun.thy	Tue Apr 03 19:31:48 2007 +0200
     2.2 +++ b/src/HOL/Fun.thy	Wed Apr 04 00:10:59 2007 +0200
     2.3 @@ -579,7 +579,7 @@
     2.4      simp_tac (Simplifier.inherit_context ss current_ss) 1
     2.5  in
     2.6    val fun_upd2_simproc =
     2.7 -    Simplifier.simproc (Theory.sign_of (the_context ()))
     2.8 +    Simplifier.simproc @{theory}
     2.9        "fun_upd2" ["f(v := w, x := y)"]
    2.10        (fn _ => fn ss => fn t =>
    2.11          case find_double t of (T, NONE) => NONE
     3.1 --- a/src/HOL/Product_Type.thy	Tue Apr 03 19:31:48 2007 +0200
     3.2 +++ b/src/HOL/Product_Type.thy	Wed Apr 04 00:10:59 2007 +0200
     3.3 @@ -433,10 +433,8 @@
     3.4          | NONE => NONE)
     3.5    |   eta_proc _ _ = NONE;
     3.6  in
     3.7 -  val split_beta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
     3.8 -    "split_beta" ["split f z"] (K beta_proc);
     3.9 -  val split_eta_proc = Simplifier.simproc (Theory.sign_of (the_context ()))
    3.10 -    "split_eta" ["split f"] (K eta_proc);
    3.11 +  val split_beta_proc = Simplifier.simproc @{theory} "split_beta" ["split f z"] (K beta_proc);
    3.12 +  val split_eta_proc = Simplifier.simproc @{theory} "split_eta" ["split f"] (K eta_proc);
    3.13  end;
    3.14  
    3.15  Addsimprocs [split_beta_proc, split_eta_proc];
     4.1 --- a/src/HOLCF/Pcpo.thy	Tue Apr 03 19:31:48 2007 +0200
     4.2 +++ b/src/HOLCF/Pcpo.thy	Wed Apr 04 00:10:59 2007 +0200
     4.3 @@ -206,8 +206,7 @@
     4.4        | _ => SOME meta_UU_reorient;
     4.5  in
     4.6    val UU_reorient_simproc = 
     4.7 -    Simplifier.simproc (the_context ())
     4.8 -      "UU_reorient_simproc" ["UU=x"] reorient_proc
     4.9 +    Simplifier.simproc @{theory} "UU_reorient_simproc" ["UU=x"] reorient_proc
    4.10  end;
    4.11  
    4.12  Addsimprocs [UU_reorient_simproc];