--- a/src/HOL/Library/refute.ML Fri Sep 12 07:38:15 2014 +0200
+++ b/src/HOL/Library/refute.ML Fri Sep 12 11:17:06 2014 +0200
@@ -1947,7 +1947,7 @@
^ Syntax.string_of_typ ctxt (Type (s', Ts'))
^ ") is not a variable")
else ()
- (* split the constructors into those occuring before/after *)
+ (* split the constructors into those occurring before/after *)
(* 'Const (s, T)' *)
val (constrs1, constrs2) = take_prefix (fn (cname, ctypes) =>
not (cname = s andalso Sign.typ_instance thy (T,
--- a/src/HOL/Tools/prop_logic.ML Fri Sep 12 07:38:15 2014 +0200
+++ b/src/HOL/Tools/prop_logic.ML Fri Sep 12 11:17:06 2014 +0200
@@ -105,7 +105,7 @@
| indices (And (fm1, fm2)) = union (op =) (indices fm1) (indices fm2);
(* ------------------------------------------------------------------------- *)
-(* maxidx: computes the maximal variable index occuring in a formula of *)
+(* maxidx: computes the maximal variable index occurring in a formula of *)
(* propositional logic 'fm'; 0 if 'fm' contains no variable *)
(* ------------------------------------------------------------------------- *)