Thm.invoke_oracle_i;
authorwenzelm
Thu Apr 07 09:26:55 2005 +0200 (2005-04-07 ago)
changeset 15667b7bdc1651198
parent 15666 5c5925dc4921
child 15668 53c049a365cf
Thm.invoke_oracle_i;
src/Pure/Isar/skip_proof.ML
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Thu Apr 07 09:26:48 2005 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Thu Apr 07 09:26:55 2005 +0200
     1.3 @@ -38,14 +38,14 @@
     1.4    if ! quick_and_dirty then t
     1.5    else error "Proof may be skipped in quick_and_dirty mode only!";
     1.6  
     1.7 -val setup = [Theory.add_oracle (skip_proofN, skip_proof)];
     1.8 +val setup =
     1.9 +  [PureThy.global_path, Theory.add_oracle (skip_proofN, skip_proof), PureThy.local_path];
    1.10  
    1.11  
    1.12  (* basic cheating *)
    1.13  
    1.14  fun make_thm thy t =
    1.15 -  (*dynamic scoping of the oracle, cannot even qualify the name due to Pure/CPure!*)
    1.16 -  Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof t);
    1.17 +  Thm.invoke_oracle_i thy skip_proofN (Theory.sign_of thy, SkipProof t);
    1.18  
    1.19  fun cheat_tac thy st =
    1.20    ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;