--- a/src/HOL/Induct/Exp.ML Tue Jan 19 11:16:39 1999 +0100
+++ b/src/HOL/Induct/Exp.ML Tue Jan 19 11:18:11 1999 +0100
@@ -9,11 +9,12 @@
AddSIs [eval.N, eval.X];
AddIs [eval.Op, eval.valOf];
-val eval_elim_cases = map (eval.mk_cases exp.simps)
- ["(N(n),sigma) -|-> (n',s')", "(X(x),sigma) -|-> (n,s')",
- "(Op f a1 a2,sigma) -|-> (n,s')",
- "(VALOF c RESULTIS e, s) -|-> (n, s1)"
- ];
+val eval_elim_cases =
+ map eval.mk_cases
+ ["(N(n),sigma) -|-> (n',s')",
+ "(X(x),sigma) -|-> (n,s')",
+ "(Op f a1 a2,sigma) -|-> (n,s')",
+ "(VALOF c RESULTIS e, s) -|-> (n, s1)"];
AddSEs eval_elim_cases;