src/HOL/Tools/Predicate_Compile/predicate_compile.ML
changeset 33126 bb8806eb5da7
parent 33125 2fef4f9429f7
child 33127 eb91ec1ef6f0
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Sat Oct 24 16:55:42 2009 +0200
@@ -83,7 +83,7 @@
     val intross4 = map (maps remove_pointless_clauses) intross3
     val _ = print_intross options thy''' "After removing pointless clauses: " intross4
     val intross5 = map (map (AxClass.overload thy''')) intross4
-    val intross6 = burrow (map (expand_tuples thy''')) intross5
+    val intross6 = map (map (expand_tuples thy''')) intross5
     val _ = print_intross options thy''' "introduction rules before registering: " intross6
     val _ = print_step options "Registering introduction rules..."
     val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy'''