# HG changeset patch
# User wenzelm
# Date 1243449316 -7200
# Node ID 4ed31c673baf9db596a97fead85d31184bc2648b
# Parent  4c34331a88f9495645747e60a0368af5f16e5afa
fixed superficial ML lapses introduced in b3c7044d47b6;

diff -r 4c34331a88f9 -r 4ed31c673baf src/HOL/Import/import_package.ML
--- a/src/HOL/Import/import_package.ML	Mon May 25 12:49:18 2009 +0200
+++ b/src/HOL/Import/import_package.ML	Wed May 27 20:35:16 2009 +0200
@@ -26,7 +26,7 @@
 
 fun import_tac ctxt (thyname, thmname) =
     if ! quick_and_dirty
-    then SkipProof.cheat_tac
+    then SkipProof.cheat_tac (ProofContext.theory_of ctxt)
     else
      fn th =>
         let
diff -r 4c34331a88f9 -r 4ed31c673baf src/HOL/Import/shuffler.ML
--- a/src/HOL/Import/shuffler.ML	Mon May 25 12:49:18 2009 +0200
+++ b/src/HOL/Import/shuffler.ML	Wed May 27 20:35:16 2009 +0200
@@ -646,8 +646,11 @@
                                   else no_tac)) st
     end
 
-fun shuffle_tac ctxt thms = gen_shuffle_tac ctxt false (map (pair "") thms);
-fun search_tac ctxt = gen_shuffle_tac thy true (map (pair "premise") (Assumption.all_prems_of ctxt);
+fun shuffle_tac ctxt thms =
+  gen_shuffle_tac ctxt false (map (pair "") thms);
+
+fun search_tac ctxt =
+  gen_shuffle_tac ctxt true (map (pair "premise") (Assumption.all_prems_of ctxt));
 
 fun add_shuffle_rule thm thy =
     let
@@ -663,7 +666,7 @@
 
 val setup =
   Method.setup @{binding shuffle_tac}
-    (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (shuffle_tac ctxt thms)))
+    (Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (shuffle_tac ctxt ths)))
     "solve goal by shuffling terms around" #>
   Method.setup @{binding search_tac}
     (Scan.succeed (SIMPLE_METHOD' o search_tac)) "search for suitable theorems" #>