# HG changeset patch
# User blanchet
# Date 1410513407 -7200
# Node ID f13f6e27d68e3c0707107c4694ef181ed4120b1d
# Parent  f95754ca70825a8f3ce0e6e7f2f8e34aa6596987
fixed spellings

diff -r f95754ca7082 -r f13f6e27d68e src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Thu Sep 11 21:11:03 2014 +0200
+++ b/src/HOL/Library/refute.ML	Fri Sep 12 11:16:47 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,
diff -r f95754ca7082 -r f13f6e27d68e src/HOL/Tools/prop_logic.ML
--- a/src/HOL/Tools/prop_logic.ML	Thu Sep 11 21:11:03 2014 +0200
+++ b/src/HOL/Tools/prop_logic.ML	Fri Sep 12 11:16:47 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             *)
 (* ------------------------------------------------------------------------- *)