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