src/HOLCF/HOLCF.thy
changeset 29354 642cac18e155
parent 29138 661a8db7e647
child 29511 7071b017cb35
child 29530 9905b660612b
     1.1 --- a/src/HOLCF/HOLCF.thy	Mon Jan 05 07:54:16 2009 -0800
     1.2 +++ b/src/HOLCF/HOLCF.thy	Mon Jan 05 18:13:26 2009 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4  declaration {* fn _ =>
     1.5    Simplifier.map_ss (fn simpset => simpset addSolver
     1.6      (mk_solver' "adm_tac" (fn ss =>
     1.7 -      adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
     1.8 +      Adm.adm_tac (cut_facts_tac (Simplifier.prems_of_ss ss) THEN' cont_tacRs ss))));
     1.9  *}
    1.10  
    1.11  end