src/Pure/Isar/skip_proof.ML
changeset 42409 3e1e80df6a42
parent 42360 da8817d01e7c
child 46045 332cb37cfcee
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Tue Apr 19 21:55:42 2011 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Tue Apr 19 22:08:42 2011 +0200
     1.3 @@ -7,6 +7,7 @@
     1.4  
     1.5  signature SKIP_PROOF =
     1.6  sig
     1.7 +  val make_thm_cterm: cterm -> thm
     1.8    val make_thm: theory -> term -> thm
     1.9    val cheat_tac: theory -> tactic
    1.10    val prove: Proof.context -> string list -> term list -> term ->
    1.11 @@ -20,14 +21,14 @@
    1.12  
    1.13  (* oracle setup *)
    1.14  
    1.15 -val (_, skip_proof) = Context.>>> (Context.map_theory_result
    1.16 -  (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) => Thm.cterm_of thy prop)));
    1.17 +val (_, make_thm_cterm) =
    1.18 +  Context.>>> (Context.map_theory_result (Thm.add_oracle (Binding.name "skip_proof", I)));
    1.19 +
    1.20 +fun make_thm thy prop = make_thm_cterm (Thm.cterm_of thy prop);
    1.21  
    1.22  
    1.23  (* basic cheating *)
    1.24  
    1.25 -fun make_thm thy prop = skip_proof (thy, prop);
    1.26 -
    1.27  fun cheat_tac thy st =
    1.28    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;
    1.29