--- a/src/Provers/project_rule.ML Thu Jun 15 18:35:16 2006 +0200
+++ b/src/Provers/project_rule.ML Thu Jun 15 23:08:54 2006 +0200
@@ -37,7 +37,7 @@
(case try imp th of
NONE => (k, th)
| SOME th' => prems (k + 1) th');
- val ([rule], ctxt') = ProofContext.import true [raw_rule] ctxt;
+ val ([rule], ctxt') = Variable.import true [raw_rule] ctxt;
fun result i =
rule
|> proj i
@@ -57,7 +57,7 @@
(case try conj2 th of
NONE => k
| SOME th' => projs (k + 1) th');
- val ([rule], _) = ProofContext.import true [raw_rule] ctxt;
+ val ([rule], _) = Variable.import true [raw_rule] ctxt;
in projects ctxt (1 upto projs 1 rule) raw_rule end;
end;