src/HOLCF/adm.ML

 
 (*** NOTE: when the following two functions are called, all terms in the list
      are equal (only their "paths" differ!)
 ***)
 
+val HOLCF_sg = sign_of HOLCF.thy;
+val chfinS = Sign.intern_sort HOLCF_sg ["chfin"];
+val pcpoS  = Sign.intern_sort HOLCF_sg ["pcpo"];
+val cont_name = Sign.intern_const (sign_of HOLCF.thy) "cont";
+val  adm_name = Sign.intern_const (sign_of HOLCF.thy)  "adm";
+
+
 (*** check whether type of terms in list is chain finite ***)
 
 fun is_chfin sign T params ((t, _)::_) =
   let val {tsig, ...} = Sign.rep_sg sign;
       val parTs = map snd (rev params)
-  in Type.of_sort tsig (fastype_of1 (T::parTs, t), ["chfin", "pcpo"]) end;
+  in Type.of_sort tsig (fastype_of1 (T::parTs, t), [hd chfinS, hd pcpoS]) end;
 
 
 (*** try to prove that terms in list are continuous
      if successful, add continuity theorem to list l ***)
 
 fun prove_cont tac sign s T prems params (l, ts as ((t, _)::_)) =
   (let val parTs = map snd (rev params);
        val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT;
        fun mk_all [] t = t
          | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t));
-       val t = HOLogic.mk_Trueprop ((Const ("cont", contT)) $ (Abs (s, T, t)));
+       val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t)));
        val t' = mk_all params (Logic.list_implies (prems, t));
        val thm = prove_goalw_cterm [] (cterm_of sign t')
                   (fn ps => [cut_facts_tac ps 1, tac 1])
    in (ts, thm)::l end) handle _ => l;
 

 
 (*** extract subgoal i from proof state ***)
 
 fun nth_subgoal i thm = nth_elem (i-1, prems_of thm);
 
-
 in
 
 (*** the admissibility tactic
      NOTE:
        (compose_tac (false, rule, 2) i) THEN

 fun adm_tac tac i state =
   state |>
     let val goali = nth_subgoal i state
     in
       case Logic.strip_assums_concl goali of
-         ((Const _) $ ((Const ("adm", _)) $ (Abs (s, T, t)))) =>
+         ((Const _) $ ((Const (name, _)) $ (Abs (s, T, t)))) =>
            let val {sign, ...} = rep_thm state;
                val prems = Logic.strip_assums_hyp goali;
                val params = Logic.strip_params goali;
                val ts = find_subterms t 0 [];
                val ts' = filter eq_terms ts;
                val ts'' = filter (is_chfin sign T params) ts';
                val thms = foldl (prove_cont tac sign s T prems params) ([], ts'')
-           in case thms of
+           in if name = adm_name then case thms of
                  ((ts as ((t', _)::_), cont_thm)::_) =>
                    let val paths = map snd ts;
                        val rule = inst_adm_subst_thm state i params s T t' t paths;
                    in
                      (compose_tac (false, rule, 2) i) THEN
                      (rtac cont_thm i) THEN
                      (REPEAT (assume_tac i)) THEN
                      (rtac adm_chain_finite i)
                    end 
                | [] => no_tac
+	      else no_tac
            end
        | _ => no_tac
     end;
 
 end;