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