src/Pure/Isar/locale.ML
changeset 28020 1ff5167592ba
parent 28005 0e71a3b1b396
child 28024 d1c2fa105443
--- a/src/Pure/Isar/locale.ML	Wed Aug 27 11:49:50 2008 +0200
+++ b/src/Pure/Isar/locale.ML	Wed Aug 27 12:00:28 2008 +0200
@@ -1595,10 +1595,10 @@
     val id' = prep_id id
     val eqns' = case get_reg id'
       of NONE => eqns
-	| SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
+        | SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
             handle Termtab.DUP t =>
-	      error ("Conflicting interpreting equations for term " ^
-		quote (Syntax.string_of_term ctxt t))
+              error ("Conflicting interpreting equations for term " ^
+                quote (Syntax.string_of_term ctxt t))
   in ((id', eqns'), eqns') end;