changeset 23577 | c5b93c69afd3 |
parent 22790 | e1cff9268177 |
child 23590 | ad95084a5c63 |
--- a/src/HOL/Tools/inductive_realizer.ML Thu Jul 05 00:06:13 2007 +0200 +++ b/src/HOL/Tools/inductive_realizer.ML Thu Jul 05 00:06:14 2007 +0200 @@ -236,7 +236,7 @@ end; fun add_dummy name dname (x as (_, (vs, s, mfx, cs))) = - if name = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs)) + if (name: string) = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs)) else x; fun add_dummies f [] _ thy =