--- a/src/HOL/Tools/prop_logic.ML Wed Feb 23 14:04:53 2005 +0100
+++ b/src/HOL/Tools/prop_logic.ML Wed Feb 23 15:00:03 2005 +0100
@@ -109,14 +109,6 @@
| maxidx (And (fm1,fm2)) = Int.max (maxidx fm1, maxidx fm2);
(* ------------------------------------------------------------------------- *)
-(* exception SAME: raised to indicate that the return value of a function is *)
-(* identical to its argument (optimization to allow sharing, *)
-(* rather than copying) *)
-(* ------------------------------------------------------------------------- *)
-
- exception SAME;
-
-(* ------------------------------------------------------------------------- *)
(* nnf: computes the negation normal form of a formula 'fm' of propositional *)
(* logic (i.e. only variables may be negated, but not subformulas) *)
(* ------------------------------------------------------------------------- *)