| changeset 26342 | 0f65fa163304 |
| parent 22819 | a7b425bb668c |
| child 26939 | 1035c89b4c02 |
--- a/src/HOL/Modelcheck/MuckeSyn.thy Wed Mar 19 22:47:39 2008 +0100 +++ b/src/HOL/Modelcheck/MuckeSyn.thy Wed Mar 19 22:50:42 2008 +0100 @@ -221,7 +221,7 @@ Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"] (fn _ => fn _ => fn t => case t of Abs _ => SOME pair_eta_expand | _ => NONE); -val Mucke_ss = simpset() addsimprocs [pair_eta_expand_proc] addsimps [Let_def]; +val Mucke_ss = @{simpset} addsimprocs [pair_eta_expand_proc] addsimps [Let_def]; (* the interface *)