src/ZF/ex/Primrec.ML

     nat_typechecks @ list.intrs @ 
     [lam_type, list_case_type, drop_type, map_type, apply_type, rec_type];
 
 (** Useful special cases of evaluation ***)
 
-simpset := !simpset setsolver (type_auto_tac pr_typechecks);
+simpset := !simpset setSolver (type_auto_tac pr_typechecks);
 
 goalw Primrec.thy [SC_def]
     "!!x l. [| x:nat;  l: list(nat) |] ==> SC ` (Cons(x,l)) = succ(x)";
 by (Asm_simp_tac 1);
 qed "SC";

 (*** Inductive definition of the PR functions ***)
 
 (* c: primrec ==> c: list(nat) -> nat *)
 val primrec_into_fun = primrec.dom_subset RS subsetD;
 
-simpset := !simpset setsolver (type_auto_tac ([primrec_into_fun] @ 
+simpset := !simpset setSolver (type_auto_tac ([primrec_into_fun] @ 
 					      pr_typechecks @ primrec.intrs));
 
 goalw Primrec.thy [ACK_def] "!!i. i:nat ==> ACK(i): primrec";
 by (etac nat_induct 1);
 by (ALLGOALS Asm_simp_tac);