1.1 --- a/src/Tools/project_rule.ML	Wed Jun 24 20:52:49 2009 +0200
     1.2 +++ b/src/Tools/project_rule.ML	Wed Jun 24 21:28:02 2009 +0200
     1.3 @@ -39,7 +39,7 @@
     1.4        (case try imp th of
     1.5          NONE => (k, th)
     1.6        | SOME th' => prems (k + 1) th');
     1.7 -    val ((_, [rule]), ctxt') = Variable.import_thms true [raw_rule] ctxt;
     1.8 +    val ((_, [rule]), ctxt') = Variable.import true [raw_rule] ctxt;
     1.9      fun result i =
    1.10        rule
    1.11        |> proj i
    1.12 @@ -59,7 +59,7 @@
    1.13        (case try conj2 th of
    1.14          NONE => k
    1.15        | SOME th' => projs (k + 1) th');
    1.16 -    val ((_, [rule]), _) = Variable.import_thms true [raw_rule] ctxt;
    1.17 +    val ((_, [rule]), _) = Variable.import true [raw_rule] ctxt;
    1.18    in projects ctxt (1 upto projs 1 rule) raw_rule end;
    1.19  
    1.20  end;