src/Provers/classical.ML
changeset 6556 daa00919502b
parent 6502 bc30e13b36a8
child 6955 9e2d97ef55d2
     1.1 --- a/src/Provers/classical.ML	Fri Apr 30 18:09:33 1999 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri Apr 30 18:10:03 1999 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4    val clasetK: Object.kind
     1.5    exception ClasetData of Object.T ref
     1.6    val setup: (theory -> theory) list
     1.7 -  val fix_methods: Object.T * (Object.T -> Object.T) *
     1.8 +  val fix_methods: Object.T * (Object.T -> Object.T) * (Object.T -> Object.T) *
     1.9      (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit) -> unit
    1.10  end;
    1.11  
    1.12 @@ -181,18 +181,20 @@
    1.13    fun undef _ = raise Match;
    1.14  
    1.15    val empty_ref = ref ERROR;
    1.16 +  val copy_fn = ref (undef: Object.T -> Object.T);
    1.17    val prep_ext_fn = ref (undef: Object.T -> Object.T);
    1.18    val merge_fn = ref (undef: Object.T * Object.T -> Object.T);
    1.19    val print_fn = ref (undef: Sign.sg -> Object.T -> unit);
    1.20  
    1.21    val empty = ClasetData empty_ref;
    1.22 +  fun copy exn = ! copy_fn exn;
    1.23    fun prep_ext exn = ! prep_ext_fn exn;
    1.24    fun merge exn = ! merge_fn exn;
    1.25    fun print sg exn = ! print_fn sg exn;
    1.26  in
    1.27 -  val setup = [Theory.init_data clasetK (empty, prep_ext, merge, print)];
    1.28 -  fun fix_methods (e, ext, mrg, prt) =
    1.29 -    (empty_ref := e; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt);
    1.30 +  val setup = [Theory.init_data clasetK (empty, copy, prep_ext, merge, print)];
    1.31 +  fun fix_methods (e, cp, ext, mrg, prt) =
    1.32 +    (empty_ref := e; copy_fn := cp; prep_ext_fn := ext; merge_fn := mrg; print_fn := prt);
    1.33  end;
    1.34  
    1.35  
    1.36 @@ -787,15 +789,16 @@
    1.37    val empty = CSData (ref empty_cs);
    1.38  
    1.39    (*create new references*)
    1.40 -  fun prep_ext (ClasetData (ref (CSData (ref cs)))) =
    1.41 +  fun copy (ClasetData (ref (CSData (ref cs)))) =
    1.42      ClasetData (ref (CSData (ref cs)));
    1.43 +  val prep_ext = copy;
    1.44  
    1.45    fun merge (ClasetData (ref (CSData (ref cs1))), ClasetData (ref (CSData (ref cs2)))) =
    1.46      ClasetData (ref (CSData (ref (merge_cs (cs1, cs2)))));
    1.47  
    1.48    fun print (_: Sign.sg) (ClasetData (ref (CSData (ref cs)))) = print_cs cs;
    1.49  in
    1.50 -  val _ = fix_methods (empty, prep_ext, merge, print);
    1.51 +  val _ = fix_methods (empty, copy, prep_ext, merge, print);
    1.52  end;
    1.53  
    1.54