src/Pure/Proof/extraction.ML
changeset 33522 737589bb9bb8
parent 33388 d64545e6cba5
child 33704 6aeb8454efc1
     1.1 --- a/src/Pure/Proof/extraction.ML	Sun Nov 08 18:43:22 2009 +0100
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sun Nov 08 18:43:42 2009 +0100
     1.3 @@ -167,7 +167,7 @@
     1.4  
     1.5  (* theory data *)
     1.6  
     1.7 -structure ExtractionData = TheoryDataFun
     1.8 +structure ExtractionData = Theory_Data
     1.9  (
    1.10    type T =
    1.11      {realizes_eqns : rules,
    1.12 @@ -187,20 +187,19 @@
    1.13       defs = [],
    1.14       expand = [],
    1.15       prep = NONE};
    1.16 -  val copy = I;
    1.17    val extend = I;
    1.18  
    1.19 -  fun merge _
    1.20 -    (({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
    1.21 +  fun merge
    1.22 +    ({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
    1.23         realizers = realizers1, defs = defs1, expand = expand1, prep = prep1},
    1.24        {realizes_eqns = realizes_eqns2, typeof_eqns = typeof_eqns2, types = types2,
    1.25 -       realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T * T) =
    1.26 +       realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T =
    1.27      {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
    1.28       typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
    1.29       types = AList.merge (op =) (K true) (types1, types2),
    1.30       realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
    1.31       defs = Library.merge Thm.eq_thm (defs1, defs2),
    1.32 -     expand = Library.merge (op =) (expand1, expand2),
    1.33 +     expand = Library.merge (op =) (expand1, expand2),   (* FIXME proper aconv !?! *)
    1.34       prep = (case prep1 of NONE => prep2 | _ => prep1)};
    1.35  );
    1.36