qualified name Pure.skip_proof;
authorwenzelm
Sat Apr 23 19:51:04 2005 +0200 (2005-04-23 ago)
changeset 15831aa58e4ec3a1f
parent 15830 74d8412b1a27
child 15832 df958c7afe50
qualified name Pure.skip_proof;
src/Pure/Isar/skip_proof.ML
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Sat Apr 23 19:50:51 2005 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Sat Apr 23 19:51:04 2005 +0200
     1.3 @@ -29,22 +29,19 @@
     1.4  
     1.5  (* oracle setup *)
     1.6  
     1.7 -val skip_proofN = "skip_proof";
     1.8 -
     1.9  exception SkipProof of term;
    1.10  
    1.11  fun skip_proof (_, SkipProof t) =
    1.12    if ! quick_and_dirty then t
    1.13    else error "Proof may be skipped in quick_and_dirty mode only!";
    1.14  
    1.15 -val _ = Context.add_setup
    1.16 - [PureThy.global_path, Theory.add_oracle (skip_proofN, skip_proof), PureThy.local_path];
    1.17 +val _ = Context.add_setup [Theory.add_oracle ("skip_proof", skip_proof)];
    1.18  
    1.19  
    1.20  (* basic cheating *)
    1.21  
    1.22  fun make_thm thy t =
    1.23 -  Thm.invoke_oracle_i thy skip_proofN (Theory.sign_of thy, SkipProof t);
    1.24 +  Thm.invoke_oracle_i thy "Pure.skip_proof" (Theory.sign_of thy, SkipProof t);
    1.25  
    1.26  fun cheat_tac thy st =
    1.27    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;