Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Thm.invoke_oracle_i;
authorwenzelm
Thu, 07 Apr 2005 09:26:55 +0200
changeset 15667 b7bdc1651198
parent 15666 5c5925dc4921
child 15668 53c049a365cf
Thm.invoke_oracle_i;
src/Pure/Isar/skip_proof.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle