src/Tools/project_rule.ML
changeset 31794 71af1fd6a5e4
parent 30160 5f7b17941730
child 32172 c4e55f30d527
--- a/src/Tools/project_rule.ML	Wed Jun 24 20:52:49 2009 +0200
+++ b/src/Tools/project_rule.ML	Wed Jun 24 21:28:02 2009 +0200
@@ -39,7 +39,7 @@
       (case try imp th of
         NONE => (k, th)
       | SOME th' => prems (k + 1) th');
-    val ((_, [rule]), ctxt') = Variable.import_thms true [raw_rule] ctxt;
+    val ((_, [rule]), ctxt') = Variable.import true [raw_rule] ctxt;
     fun result i =
       rule
       |> proj i
@@ -59,7 +59,7 @@
       (case try conj2 th of
         NONE => k
       | SOME th' => projs (k + 1) th');
-    val ((_, [rule]), _) = Variable.import_thms true [raw_rule] ctxt;
+    val ((_, [rule]), _) = Variable.import true [raw_rule] ctxt;
   in projects ctxt (1 upto projs 1 rule) raw_rule end;
 
 end;