src/Tools/project_rule.ML
changeset 33368 b1cf34f1855c
parent 32172 c4e55f30d527
     1.1 --- a/src/Tools/project_rule.ML	Fri Oct 30 18:33:21 2009 +0100
     1.2 +++ b/src/Tools/project_rule.ML	Sun Nov 01 15:24:45 2009 +0100
     1.3 @@ -47,8 +47,8 @@
     1.4          Thm.permute_prems 0 (~ k)
     1.5          #> singleton (Variable.export ctxt' ctxt)
     1.6          #> Drule.zero_var_indexes
     1.7 -        #> RuleCases.save raw_rule
     1.8 -        #> RuleCases.add_consumes k);
     1.9 +        #> Rule_Cases.save raw_rule
    1.10 +        #> Rule_Cases.add_consumes k);
    1.11    in map result is end;
    1.12  
    1.13  fun project ctxt i th = hd (projects ctxt [i] th);