src/Provers/classical.ML
changeset 24358 d75af3e90e82
parent 24218 fbf1646b267c
child 24867 e5b55d7be9bb
     1.1 --- a/src/Provers/classical.ML	Mon Aug 20 20:38:32 2007 +0200
     1.2 +++ b/src/Provers/classical.ML	Mon Aug 20 20:43:58 2007 +0200
     1.3 @@ -655,22 +655,24 @@
     1.4    Merging the term nets may look more efficient, but the rather delicate
     1.5    treatment of priority might get muddled up.*)
     1.6  fun merge_cs (cs as CS {safeIs, safeEs, hazIs, hazEs, ...},
     1.7 -    CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
     1.8 +    cs' as CS {safeIs = safeIs2, safeEs = safeEs2, hazIs = hazIs2, hazEs = hazEs2,
     1.9        swrappers, uwrappers, ...}) =
    1.10 -  let
    1.11 -    val safeIs' = fold rem_thm safeIs safeIs2;
    1.12 -    val safeEs' = fold rem_thm safeEs safeEs2;
    1.13 -    val hazIs' = fold rem_thm hazIs hazIs2;
    1.14 -    val hazEs' = fold rem_thm hazEs hazEs2;
    1.15 -    val cs1   = cs addSIs safeIs'
    1.16 -                   addSEs safeEs'
    1.17 -                   addIs  hazIs'
    1.18 -                   addEs  hazEs';
    1.19 -    val cs2 = map_swrappers
    1.20 -      (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
    1.21 -    val cs3 = map_uwrappers
    1.22 -      (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
    1.23 -  in cs3 end;
    1.24 +  if pointer_eq (cs, cs') then cs
    1.25 +  else
    1.26 +    let
    1.27 +      val safeIs' = fold rem_thm safeIs safeIs2;
    1.28 +      val safeEs' = fold rem_thm safeEs safeEs2;
    1.29 +      val hazIs' = fold rem_thm hazIs hazIs2;
    1.30 +      val hazEs' = fold rem_thm hazEs hazEs2;
    1.31 +      val cs1   = cs addSIs safeIs'
    1.32 +                     addSEs safeEs'
    1.33 +                     addIs  hazIs'
    1.34 +                     addEs  hazEs';
    1.35 +      val cs2 = map_swrappers
    1.36 +        (fn ws => AList.merge (op =) (K true) (ws, swrappers)) cs1;
    1.37 +      val cs3 = map_uwrappers
    1.38 +        (fn ws => AList.merge (op =) (K true) (ws, uwrappers)) cs2;
    1.39 +    in cs3 end;
    1.40  
    1.41  
    1.42  (**** Simple tactics for theorem proving ****)
    1.43 @@ -851,12 +853,14 @@
    1.44  val empty_context_cs = make_context_cs ([], []);
    1.45  
    1.46  fun merge_context_cs (ctxt_cs1, ctxt_cs2) =
    1.47 -  let
    1.48 -    val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
    1.49 -    val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
    1.50 -    val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
    1.51 -    val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
    1.52 -  in make_context_cs (swrappers', uwrappers') end;
    1.53 +  if pointer_eq (ctxt_cs1, ctxt_cs2) then ctxt_cs1
    1.54 +  else
    1.55 +    let
    1.56 +      val ContextCS {swrappers = swrappers1, uwrappers = uwrappers1} = ctxt_cs1;
    1.57 +      val ContextCS {swrappers = swrappers2, uwrappers = uwrappers2} = ctxt_cs2;
    1.58 +      val swrappers' = AList.merge (op =) (K true) (swrappers1, swrappers2);
    1.59 +      val uwrappers' = AList.merge (op =) (K true) (uwrappers1, uwrappers2);
    1.60 +    in make_context_cs (swrappers', uwrappers') end;
    1.61  
    1.62  
    1.63