# HG changeset patch
# User huffman
# Date 1228945449 28800
# Node ID 059bdb9813c653447b580e74f461faf3907ec09b
# Parent  773098b76201be0d3394742344004483a7ea3f62
use ML antiquotations

diff -r 773098b76201 -r 059bdb9813c6 src/HOLCF/Tools/cont_proc.ML
--- a/src/HOLCF/Tools/cont_proc.ML	Wed Dec 10 12:31:35 2008 -0800
+++ b/src/HOLCF/Tools/cont_proc.ML	Wed Dec 10 13:44:09 2008 -0800
@@ -1,5 +1,4 @@
 (*  Title:      HOLCF/Tools/cont_proc.ML
-    ID:         $Id$
     Author:     Brian Huffman
 *)
 
@@ -18,11 +17,11 @@
 
 (** theory context references **)
 
-val cont_K = thm "cont_const";
-val cont_I = thm "cont_id";
-val cont_A = thm "cont2cont_Rep_CFun";
-val cont_L = thm "cont2cont_LAM";
-val cont_R = thm "cont_Rep_CFun2";
+val cont_K = @{thm cont_const};
+val cont_I = @{thm cont_id};
+val cont_A = @{thm cont2cont_Rep_CFun};
+val cont_L = @{thm cont2cont_LAM};
+val cont_R = @{thm cont_Rep_CFun2};
 
 (* checks whether a term contains no dangling bound variables *)
 val is_closed_term =
@@ -35,10 +34,11 @@
   in bound_less 0 end;
 
 (* checks whether a term is written entirely in the LCF sublanguage *)
-fun is_lcf_term (Const ("Cfun.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 ("Cfun.Abs_CFun", _) $ Abs (_, _, t)) = is_lcf_term t
-  | is_lcf_term (Const ("Cfun.Abs_CFun", _) $ _) = false
+  | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
+      is_lcf_term t
+  | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ _) = false
   | is_lcf_term (Bound _) = true
   | is_lcf_term t = is_closed_term t;
 
@@ -73,12 +73,12 @@
   (* 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 ("Cfun.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 ("Cfun.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;
@@ -114,9 +114,9 @@
       [] => no_tac thm
     | (c::cs) => (prev_cont_thms := cs; rtac c i thm));
 
-  fun cont_tac_of_term (Const ("Cont.cont", _) $ f) =
+  fun cont_tac_of_term (Const (@{const_name cont}, _) $ f) =
     let
-      val f' = Const ("Cfun.Abs_CFun", dummyT) $ f;
+      val f' = Const (@{const_name Abs_CFun}, dummyT) $ f;
     in
       if is_lcf_term f'
       then old_cont_tac ORELSE' new_cont_tac f'