src/Pure/Isar/locale.ML

 fun join_eqns get_reg prep_id ctxt id eqns =
   let
     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;
 
 
 (* collect witnesses and equations up to a particular target for global
    registration; requires parameters and flattened list of identifiers