--- 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;