--- a/src/Pure/Proof/extraction.ML Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/Proof/extraction.ML Thu Apr 27 15:06:35 2006 +0200
@@ -307,7 +307,7 @@
let
val {realizes_eqns, typeof_eqns, defs, types, ...} =
ExtractionData.get thy;
- val procs = List.concat (map (fst o snd) types);
+ val procs = maps (fst o snd) types;
val rtypes = map fst types;
val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
val thy' = add_syntax thy;
@@ -343,7 +343,7 @@
val thy' = add_syntax thy;
val {realizes_eqns, typeof_eqns, defs, types, ...} =
ExtractionData.get thy';
- val procs = List.concat (map (fst o snd) types);
+ val procs = maps (fst o snd) types;
val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
val prop' = Pattern.rewrite_term thy'
(map (Logic.dest_equals o prop_of) defs) [] prop;
@@ -460,7 +460,7 @@
val thy' = add_syntax thy;
val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
ExtractionData.get thy;
- val procs = List.concat (map (fst o snd) types);
+ val procs = maps (fst o snd) types;
val rtypes = map fst types;
val typroc = typeof_proc (Sign.defaultS thy');
val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o