src/HOLCF/Tools/Domain/domain_theorems.ML
changeset 32172 c4e55f30d527
parent 32149 ef59550a55d3
child 32740 9dd0a2f83429
     1.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Jul 24 12:33:00 2009 +0200
     1.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Fri Jul 24 18:58:58 2009 +0200
     1.3 @@ -1033,7 +1033,7 @@
     1.4      in pg [] goal (K tacs) end;
     1.5  end; (* local *)
     1.6  
     1.7 -val inducts = ProjectRule.projections (ProofContext.init thy) ind;
     1.8 +val inducts = Project_Rule.projections (ProofContext.init thy) ind;
     1.9  fun ind_rule (dname, rule) = ((Binding.empty, [rule]), [Induct.induct_type dname]);
    1.10  val induct_failed = (Thm.prop_of ind = Thm.prop_of TrueI);
    1.11