src/ZF/WF.ML
changeset 2637 e9b203f854ae
parent 2482 87383dd9f4b5
child 3016 15763781afb0
--- a/src/ZF/WF.ML	Sat Feb 15 17:48:19 1997 +0100
+++ b/src/ZF/WF.ML	Sat Feb 15 17:52:31 1997 +0100
@@ -225,7 +225,7 @@
                         eresolve_tac [underD, transD, spec RS mp]));
 
 (*** NOTE! some simplifications need a different solver!! ***)
-val wf_super_ss = !simpset setsolver indhyp_tac;
+val wf_super_ss = !simpset setSolver indhyp_tac;
 
 val prems = goalw WF.thy [is_recfun_def]
     "[| wf(r);  trans(r);  is_recfun(r,a,H,f);  is_recfun(r,b,H,g) |] ==> \