src/HOLCF/Tools/cont_proc.ML

 
 val cont_K = @{thm cont_const};
 val cont_I = @{thm cont_id};
 val cont_A = @{thm cont2cont_APP};
 val cont_L = @{thm cont2cont_LAM};
-val cont_R = @{thm cont_Rep_CFun2};
+val cont_R = @{thm cont_Rep_cfun2};
 
 (* checks whether a term contains no dangling bound variables *)
 fun is_closed_term t = not (Term.loose_bvar (t, 0));
 
 (* checks whether a term is written entirely in the LCF sublanguage *)
-fun is_lcf_term (Const (@{const_name Rep_CFun}, _) $ t $ u) =
+fun is_lcf_term (Const (@{const_name Rep_cfun}, _) $ t $ u) =
       is_lcf_term t andalso is_lcf_term u
-  | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
+  | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) =
       is_lcf_term t
-  | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ t) =
+  | is_lcf_term (Const (@{const_name Abs_cfun}, _) $ t) =
       is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
   | is_lcf_term (Bound _) = true
   | is_lcf_term t = is_closed_term t;
 
 (*

     in (map (fn y => SOME (k y RS Lx)) ys, x') end;
 
   (* first list: cont thm for each dangling bound variable *)
   (* second list: cont thm for each LAM in t *)
   (* if b = false, only return cont thm for outermost LAMs *)
-  fun cont_thms1 b (Const (@{const_name Rep_CFun}, _) $ f $ t) =
+  fun cont_thms1 b (Const (@{const_name Rep_cfun}, _) $ f $ t) =
     let
       val (cs1,ls1) = cont_thms1 b f;
       val (cs2,ls2) = cont_thms1 b t;
     in (zip cs1 cs2, if b then ls1 @ ls2 else []) end
-    | cont_thms1 b (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
+    | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ Abs (_, _, t)) =
     let
       val (cs, ls) = cont_thms1 b t;
       val (cs', l) = lam cs;
     in (cs', l::ls) end
-    | cont_thms1 b (Const (@{const_name Abs_CFun}, _) $ t) =
+    | cont_thms1 b (Const (@{const_name Abs_cfun}, _) $ t) =
     let
       val t' = Term.incr_boundvars 1 t $ Bound 0;
       val (cs, ls) = cont_thms1 b t';
       val (cs', l) = lam cs;
     in (cs', l::ls) end

         [] => no_tac
       | (c::cs) => rtac c i;
 
     fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
       let
-        val f' = Const (@{const_name Abs_CFun}, dummyT) $ f;
+        val f' = Const (@{const_name Abs_cfun}, dummyT) $ f;
       in
         if is_lcf_term f'
         then new_cont_tac f'
         else REPEAT_ALL_NEW (resolve_tac rules)
       end