src/Pure/Proof/extraction.ML
changeset 22717 74dbc7696083
parent 22675 acf10be7dcca
child 22750 bff5d59de79b
     1.1 --- a/src/Pure/Proof/extraction.ML	Mon Apr 16 12:16:11 2007 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Mon Apr 16 16:11:03 2007 +0200
     1.3 @@ -204,7 +204,7 @@
     1.4         realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T * T) =
     1.5      {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
     1.6       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
     1.7 -     types = merge_alists types1 types2,
     1.8 +     types = AList.merge (op =) (K true) (types1, types2),
     1.9       realizers = Symtab.merge_list (gen_eq_set (op =) o pairself #1) (realizers1, realizers2),
    1.10       defs = Library.merge Thm.eq_thm (defs1, defs2),
    1.11       expand = Library.merge (op =) (expand1, expand2),
    1.12 @@ -343,7 +343,7 @@
    1.13      val thy' = add_syntax thy;
    1.14      val {realizes_eqns, typeof_eqns, defs, types, ...} =
    1.15        ExtractionData.get thy';
    1.16 -    val procs = maps (fst o snd) types;
    1.17 +    val procs = maps (rev o fst o snd) types;
    1.18      val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
    1.19      val prop' = Pattern.rewrite_term thy'
    1.20        (map (Logic.dest_equals o prop_of) defs) [] prop;
    1.21 @@ -390,14 +390,12 @@
    1.22  (** types with computational content **)
    1.23  
    1.24  fun add_types tys thy =
    1.25 -  let val {realizes_eqns, typeof_eqns, types, realizers,
    1.26 -    defs, expand, prep} = ExtractionData.get thy;
    1.27 -  in
    1.28 -    ExtractionData.put
    1.29 +  ExtractionData.map
    1.30 +    (fn {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =>
    1.31        {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns,
    1.32 -       types = map (apfst (Sign.intern_type thy)) tys @ types,
    1.33 -       realizers = realizers, defs = defs, expand = expand, prep = prep} thy
    1.34 -  end;
    1.35 +       types = fold (AList.update (op =) o apfst (Sign.intern_type thy)) tys types,
    1.36 +       realizers = realizers, defs = defs, expand = expand, prep = prep})
    1.37 +    thy;
    1.38  
    1.39  
    1.40  (** Pure setup **)
    1.41 @@ -460,7 +458,7 @@
    1.42      val thy' = add_syntax thy;
    1.43      val {realizes_eqns, typeof_eqns, types, realizers, defs, expand, prep} =
    1.44        ExtractionData.get thy;
    1.45 -    val procs = maps (fst o snd) types;
    1.46 +    val procs = maps (rev o fst o snd) types;
    1.47      val rtypes = map fst types;
    1.48      val typroc = typeof_proc (Sign.defaultS thy');
    1.49      val prep = the_default (K I) prep thy' o ProofRewriteRules.elim_defs thy' false defs o