src/HOLCF/HOLCF.ML
changeset 7570 a9391550eea1
parent 4098 71e05eb27fb6
child 9245 428385c4bc50
     1.1 --- a/src/HOLCF/HOLCF.ML	Tue Sep 21 19:10:39 1999 +0200
     1.2 +++ b/src/HOLCF/HOLCF.ML	Tue Sep 21 19:11:07 1999 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  use"adm.ML";
     1.6  
     1.7 -simpset_ref() := simpset() addSolver(fn thms =>
     1.8 -            (adm_tac (cut_facts_tac thms THEN' cont_tacRs)));
     1.9 +simpset_ref() := simpset() addSolver
    1.10 +   (mk_solver "adm_tac" (fn thms => (adm_tac (cut_facts_tac thms THEN' cont_tacRs))));
    1.11  
    1.12  val HOLCF_ss = simpset();