standardized ML aliases;

--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Sep 12 13:42:28 2012 +0200
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML	Wed Sep 12 13:56:49 2012 +0200
@@ -316,8 +316,8 @@
     fun body 0 t = t
       | body n t = body (n - 1) (t  $ (Bound (n - 1)))
   in
-    body n (Const (str, Term.dummyT))
-    |> funpow n (Term.absdummy Term.dummyT)
+    body n (Const (str, dummyT))
+    |> funpow n (Term.absdummy dummyT)
   end
 fun mk_fun_type [] b acc = acc b
   | mk_fun_type (ty :: tys) b acc =
@@ -365,10 +365,10 @@
           (string_of_interpreted_symbol interpreted_symbol))), [])
    | Interpreted_Logic logic_symbol =>
        (case logic_symbol of
-          Equals => HOLogic.eq_const Term.dummyT
+          Equals => HOLogic.eq_const dummyT
         | NEquals =>
-           HOLogic.mk_not (HOLogic.eq_const Term.dummyT $ Bound 1 $ Bound 0)
-           |> (Term.absdummy Term.dummyT #> Term.absdummy Term.dummyT)
+           HOLogic.mk_not (HOLogic.eq_const dummyT $ Bound 1 $ Bound 0)
+           |> (Term.absdummy dummyT #> Term.absdummy dummyT)
         | Or => HOLogic.disj
         | And => HOLogic.conj
         | Iff => HOLogic.eq_const HOLogic.boolT
@@ -380,8 +380,8 @@
         | Nor => @{term "\<lambda> x. \<lambda> y. \<not> (x \<or> y)"}
         | Nand => @{term "\<lambda> x. \<lambda> y. \<not> (x \<and> y)"}
         | Not => HOLogic.Not
-        | Op_Forall => HOLogic.all_const Term.dummyT
-        | Op_Exists => HOLogic.exists_const Term.dummyT
+        | Op_Forall => HOLogic.all_const dummyT
+        | Op_Exists => HOLogic.exists_const dummyT
         | True => @{term "True"}
         | False => @{term "False"}
         )
@@ -404,7 +404,7 @@
 fun mtimes thy =
   fold (fn x => fn y =>
     Sign.mk_const thy
-    ("Product_Type.Pair", [Term.dummyT, Term.dummyT]) $ y $ x)
+    ("Product_Type.Pair", [dummyT, dummyT]) $ y $ x)
 
 fun mtimes' (args, thy) f =
   let
@@ -530,7 +530,7 @@
            SOME ty =>
              (case ty of
                 SOME ty => Free (n, ty)
-              | NONE => Free (n, Term.dummyT) (*to infer the variable's type*)
+              | NONE => Free (n, dummyT) (*to infer the variable's type*)
              )
          | NONE =>
              raise MISINTERPRET_TERM ("Could not type variable", tptp_t))
@@ -621,7 +621,7 @@
                  case ty of
                    NONE =>
                      f (n,
-                        if language = THF then Term.dummyT
+                        if language = THF then dummyT
                         else
                           interpret_type config thy type_map
                            (Defined_type Type_Ind),
@@ -646,12 +646,12 @@
             let val (t, thy') =
               interpret_formula config language const_map var_types type_map
                (Quant (Lambda, bindings, tptp_formula)) thy
-            in ((HOLogic.choice_const Term.dummyT) $ t, thy') end
+            in ((HOLogic.choice_const dummyT) $ t, thy') end
         | Iota =>
             let val (t, thy') =
               interpret_formula config language const_map var_types type_map
                (Quant (Lambda, bindings, tptp_formula)) thy
-            in (Const (@{const_name The}, Term.dummyT) $ t, thy') end
+            in (Const (@{const_name The}, dummyT) $ t, thy') end
         | Dep_Prod =>
             raise MISINTERPRET_FORMULA ("Unsupported", tptp_fmla)
         | Dep_Sum =>

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Sep 12 13:42:28 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Sep 12 13:56:49 2012 +0200
@@ -380,7 +380,7 @@
 
 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
 local
-  val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
+  val choice_const = (fst o dest_Const o HOLogic.choice_const) dummyT
   fun default c = const_prefix ^ lookup_const c
 in
   fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Sep 12 13:42:28 2012 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Wed Sep 12 13:56:49 2012 +0200
@@ -38,7 +38,7 @@
   end
 
 fun pred_of_function thy name =
-  case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, Term.dummyT)) of
+  case Item_Net.retrieve (Fun_Pred.get thy) (Const (name, dummyT)) of
     [] => NONE
   | [(f, p)] => SOME (fst (dest_Const p))
   | _ => error ("Multiple matches possible for lookup of constant " ^ name)

--- a/src/HOL/Tools/numeral_simprocs.ML	Wed Sep 12 13:42:28 2012 +0200
+++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Sep 12 13:56:49 2012 +0200
@@ -57,7 +57,7 @@
 val dest_sum = Arith_Data.dest_sum;
 
 val mk_diff = HOLogic.mk_binop @{const_name Groups.minus};
-val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} Term.dummyT;
+val dest_diff = HOLogic.dest_bin @{const_name Groups.minus} dummyT;
 
 val mk_times = HOLogic.mk_binop @{const_name Groups.times};
 
@@ -79,7 +79,7 @@
 fun long_mk_prod T []        = one_of T
   | long_mk_prod T (t :: ts) = mk_times (t, mk_prod T ts);
 
-val dest_times = HOLogic.dest_bin @{const_name Groups.times} Term.dummyT;
+val dest_times = HOLogic.dest_bin @{const_name Groups.times} dummyT;
 
 fun dest_prod t =
       let val (t,u) = dest_times t
@@ -262,7 +262,7 @@
 structure EqCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val mk_bal   = HOLogic.mk_eq
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
   val bal_add1 = @{thm eq_add_iff1} RS trans
   val bal_add2 = @{thm eq_add_iff2} RS trans
 );
@@ -270,7 +270,7 @@
 structure LessCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
   val bal_add1 = @{thm less_add_iff1} RS trans
   val bal_add2 = @{thm less_add_iff2} RS trans
 );
@@ -278,7 +278,7 @@
 structure LeCancelNumerals = CancelNumeralsFun
  (open CancelNumeralsCommon
   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
   val bal_add1 = @{thm le_add_iff1} RS trans
   val bal_add2 = @{thm le_add_iff2} RS trans
 );
@@ -385,7 +385,7 @@
 structure DivCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
-  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} dummyT
   val cancel = @{thm div_mult_mult1} RS trans
   val neg_exchanges = false
 )
@@ -394,7 +394,7 @@
 structure DivideCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
-  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} dummyT
   val cancel = @{thm mult_divide_mult_cancel_left} RS trans
   val neg_exchanges = false
 )
@@ -402,7 +402,7 @@
 structure EqCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val mk_bal   = HOLogic.mk_eq
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
   val cancel = @{thm mult_cancel_left} RS trans
   val neg_exchanges = false
 )
@@ -410,7 +410,7 @@
 structure LessCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
   val cancel = @{thm mult_less_cancel_left} RS trans
   val neg_exchanges = true
 )
@@ -418,7 +418,7 @@
 structure LeCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
   val cancel = @{thm mult_le_cancel_left} RS trans
   val neg_exchanges = true
 )
@@ -501,7 +501,7 @@
 structure EqCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val mk_bal   = HOLogic.mk_eq
-  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} dummyT
   fun simp_conv _ _ = SOME @{thm mult_cancel_left}
 );
 
@@ -509,7 +509,7 @@
 structure LeCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less_eq}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} dummyT
   val simp_conv = sign_conv
     @{thm mult_le_cancel_left_pos} @{thm mult_le_cancel_left_neg}
 );
@@ -518,7 +518,7 @@
 structure LessCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val mk_bal   = HOLogic.mk_binrel @{const_name Orderings.less}
-  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} dummyT
   val simp_conv = sign_conv
     @{thm mult_less_cancel_left_pos} @{thm mult_less_cancel_left_neg}
 );
@@ -527,14 +527,14 @@
 structure DivCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.div}
-  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name Divides.div} dummyT
   fun simp_conv _ _ = SOME @{thm div_mult_mult1_if}
 );
 
 structure ModCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val mk_bal   = HOLogic.mk_binop @{const_name Divides.mod}
-  val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name Divides.mod} dummyT
   fun simp_conv _ _ = SOME @{thm mod_mult_mult1}
 );
 
@@ -542,7 +542,7 @@
 structure DvdCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val mk_bal   = HOLogic.mk_binrel @{const_name Rings.dvd}
-  val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name Rings.dvd} dummyT
   fun simp_conv _ _ = SOME @{thm dvd_mult_cancel_left}
 );
 
@@ -550,7 +550,7 @@
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
-  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
+  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} dummyT
   fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
 );