# HG changeset patch
# User haftmann
# Date 1156919370 -7200
# Node ID 110a223ba63c1f4d284fb12d15fefe71de03f363
# Parent  55471f940e5c31aa9599654d107c6b78091265dc
fixed bug in wfrec appgen

diff -r 55471f940e5c -r 110a223ba63c src/Pure/Tools/codegen_package.ML
--- a/src/Pure/Tools/codegen_package.ML	Wed Aug 30 03:30:09 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML	Wed Aug 30 08:29:30 2006 +0200
@@ -642,12 +642,10 @@
     trns
     |> ensure_def ((K o fail) "no extraction for wfrec") false ("generating wfrec") idf
     |> exprgen_type thy tabs ty'
-    ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
-           (sortlookups_const thy thmtab (c, ty))
     ||>> exprgen_type thy tabs ty_def
     ||>> exprgen_term thy tabs tf
     ||>> exprgen_term thy tabs tx
-    |-> (fn ((((_, ls), ty), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx))
+    |-> (fn (((_, ty), tf), tx) => pair (IConst (idf, ([], ty)) `$ tf `$ tx))
   end;