src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
changeset 49457 1d2825673cec
parent 49456 fa8302c8dea1
child 49463 83ac281bcdc2
--- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Thu Sep 20 02:42:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Thu Sep 20 02:42:48 2012 +0200
@@ -126,7 +126,7 @@
 
 open BNF_Tactics
 open BNF_Util
-open BNF_FP_Util
+open BNF_FP
 open BNF_GFP_Util
 
 val Pair_eq_subst_id = @{thm Pair_eq[THEN subst, of "%x. x"]};