# HG changeset patch # User wenzelm # Date 1112858815 -7200 # Node ID b7bdc1651198071dc6271957c84c4728e7cc0bcb # Parent 5c5925dc4921884334e532a038426f84a808cbbd Thm.invoke_oracle_i; diff -r 5c5925dc4921 -r b7bdc1651198 src/Pure/Isar/skip_proof.ML --- a/src/Pure/Isar/skip_proof.ML Thu Apr 07 09:26:48 2005 +0200 +++ b/src/Pure/Isar/skip_proof.ML Thu Apr 07 09:26:55 2005 +0200 @@ -38,14 +38,14 @@ if ! quick_and_dirty then t else error "Proof may be skipped in quick_and_dirty mode only!"; -val setup = [Theory.add_oracle (skip_proofN, skip_proof)]; +val setup = + [PureThy.global_path, Theory.add_oracle (skip_proofN, skip_proof), PureThy.local_path]; (* basic cheating *) fun make_thm thy t = - (*dynamic scoping of the oracle, cannot even qualify the name due to Pure/CPure!*) - Thm.invoke_oracle thy skip_proofN (Theory.sign_of thy, SkipProof t); + Thm.invoke_oracle_i thy skip_proofN (Theory.sign_of thy, SkipProof t); fun cheat_tac thy st = ALLGOALS (Tactic.rtac (make_thm thy (Var (("A", 0), propT)))) st;