--- a/src/Pure/Isar/calculation.ML Sun Nov 01 20:55:39 2009 +0100
+++ b/src/Pure/Isar/calculation.ML Sun Nov 01 20:59:34 2009 +0100
@@ -66,8 +66,8 @@
(* add/del rules *)
-val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.insert);
-val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.delete);
+val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.update);
+val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.remove);
val sym_add =
Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
@@ -131,7 +131,8 @@
fun combine ths =
(case opt_rules of SOME rules => rules
| NONE =>
- (case ths of [] => Item_Net.content (#1 (get_rules state))
+ (case ths of
+ [] => Item_Net.content (#1 (get_rules state))
| th :: _ => Item_Net.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
|> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
|> Seq.filter (not o projection ths);