src/ZF/int_arith.ML

--- a/src/ZF/int_arith.ML	Mon Feb 11 15:19:17 2008 +0100
+++ b/src/ZF/int_arith.ML	Mon Feb 11 15:40:21 2008 +0100
@@ -95,12 +95,12 @@
 
 (*Utilities*)
 
-val integ_of_const = Const ("Bin.integ_of", iT --> iT);
+val integ_of_const = Const (@{const_name "Bin.integ_of"}, iT --> iT);
 
 fun mk_numeral n = integ_of_const $ NumeralSyntax.mk_bin n;
 
 (*Decodes a binary INTEGER*)
-fun dest_numeral (Const("Bin.integ_of", _) $ w) =
+fun dest_numeral (Const(@{const_name "Bin.integ_of"}, _) $ w) =
      (NumeralSyntax.dest_bin w
       handle Match => raise TERM("Int_Numeral_Simprocs.dest_numeral:1", [w]))
   | dest_numeral t =  raise TERM("Int_Numeral_Simprocs.dest_numeral:2", [t]);
@@ -111,11 +111,11 @@
   | find_first_numeral past [] = raise TERM("find_first_numeral", []);
 
 val zero = mk_numeral 0;
-val mk_plus = FOLogic.mk_binop "Int.zadd";
+val mk_plus = FOLogic.mk_binop @{const_name "Int_ZF.zadd"};
 
 val iT = Ind_Syntax.iT;
 
-val zminus_const = Const ("Int.zminus", iT --> iT);
+val zminus_const = Const (@{const_name "Int_ZF.zminus"}, iT --> iT);
 
 (*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
 fun mk_sum []        = zero
@@ -126,30 +126,30 @@
 fun long_mk_sum []        = zero
   | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
 
-val dest_plus = FOLogic.dest_bin "Int.zadd" iT;
+val dest_plus = FOLogic.dest_bin @{const_name "Int_ZF.zadd"} iT;
 
 (*decompose additions AND subtractions as a sum*)
-fun dest_summing (pos, Const ("Int.zadd", _) $ t $ u, ts) =
+fun dest_summing (pos, Const (@{const_name "Int_ZF.zadd"}, _) $ t $ u, ts) =
         dest_summing (pos, t, dest_summing (pos, u, ts))
-  | dest_summing (pos, Const ("Int.zdiff", _) $ t $ u, ts) =
+  | dest_summing (pos, Const (@{const_name "Int_ZF.zdiff"}, _) $ t $ u, ts) =
         dest_summing (pos, t, dest_summing (not pos, u, ts))
   | dest_summing (pos, t, ts) =
         if pos then t::ts else zminus_const$t :: ts;
 
 fun dest_sum t = dest_summing (true, t, []);
 
-val mk_diff = FOLogic.mk_binop "Int.zdiff";
-val dest_diff = FOLogic.dest_bin "Int.zdiff" iT;
+val mk_diff = FOLogic.mk_binop @{const_name "Int_ZF.zdiff"};
+val dest_diff = FOLogic.dest_bin @{const_name "Int_ZF.zdiff"} iT;
 
 val one = mk_numeral 1;
-val mk_times = FOLogic.mk_binop "Int.zmult";
+val mk_times = FOLogic.mk_binop @{const_name "Int_ZF.zmult"};
 
 fun mk_prod [] = one
   | mk_prod [t] = t
   | mk_prod (t :: ts) = if t = one then mk_prod ts
                         else mk_times (t, mk_prod ts);
 
-val dest_times = FOLogic.dest_bin "Int.zmult" iT;
+val dest_times = FOLogic.dest_bin @{const_name "Int_ZF.zmult"} iT;
 
 fun dest_prod t =
       let val (t,u) = dest_times t
@@ -160,7 +160,7 @@
 fun mk_coeff (k, t) = mk_times (mk_numeral k, t);
 
 (*Express t as a product of (possibly) a numeral with other sorted terms*)
-fun dest_coeff sign (Const ("Int.zminus", _) $ t) = dest_coeff (~sign) t
+fun dest_coeff sign (Const (@{const_name "Int_ZF.zminus"}, _) $ t) = dest_coeff (~sign) t
   | dest_coeff sign t =
     let val ts = sort Term.term_ord (dest_prod t)
         val (n, ts') = find_first_numeral [] ts
@@ -254,8 +254,8 @@
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = ArithData.prove_conv "intless_cancel_numerals"
-  val mk_bal   = FOLogic.mk_binrel "Int.zless"
-  val dest_bal = FOLogic.dest_bin "Int.zless" iT
+  val mk_bal   = FOLogic.mk_binrel @{const_name "Int_ZF.zless"}
+  val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zless"} iT
   val bal_add1 = less_add_iff1 RS iff_trans
   val bal_add2 = less_add_iff2 RS iff_trans
 );
@@ -263,8 +263,8 @@
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val prove_conv = ArithData.prove_conv "intle_cancel_numerals"
-  val mk_bal   = FOLogic.mk_binrel "Int.zle"
-  val dest_bal = FOLogic.dest_bin "Int.zle" iT
+  val mk_bal   = FOLogic.mk_binrel @{const_name "Int_ZF.zle"}
+  val dest_bal = FOLogic.dest_bin @{const_name "Int_ZF.zle"} iT
   val bal_add1 = le_add_iff1 RS iff_trans
   val bal_add2 = le_add_iff2 RS iff_trans
 );