# HG changeset patch
# User blanchet
# Date 1325675393 -3600
# Node ID dd112cd72c489159c9e3433b3ee1b45fa108c9a6
# Parent  31bc296a1257c9c9fefa0ef443c6fc5db9aaa4d9
tuning

diff -r 31bc296a1257 -r dd112cd72c48 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jan 04 12:09:53 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jan 04 12:09:53 2012 +0100
@@ -1982,8 +1982,7 @@
                           $ (suc_const iter_T $ Bound 0) $ n_var)
     val x_var = Var (("x", 0), T)
     val y_var = Var (("y", 0), T)
-    fun bisim_const T =
-      Const (@{const_name bisim}, iter_T --> T --> T --> bool_T)
+    fun bisim_const T = Const (@{const_name bisim}, [iter_T, T, T] ---> bool_T)
     fun nth_sub_bisim x n nth_T =
       (if is_codatatype ctxt nth_T then bisim_const nth_T $ n_var_minus_1
        else HOLogic.eq_const nth_T)
diff -r 31bc296a1257 -r dd112cd72c48 src/HOL/Tools/Nitpick/nitrox.ML
--- a/src/HOL/Tools/Nitpick/nitrox.ML	Wed Jan 04 12:09:53 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitrox.ML	Wed Jan 04 12:09:53 2012 +0100
@@ -16,6 +16,7 @@
 open ATP_Util
 open ATP_Problem
 open ATP_Proof
+open Nitpick_Util
 open Nitpick
 open Nitpick_Isar
 
@@ -60,14 +61,13 @@
                   parse_problem))
   o tptp_explode
 
-val boolT = @{typ bool}
-val iotaT = @{typ iota}
-val quantT = (iotaT --> boolT) --> boolT
+val iota_T = @{typ iota}
+val quant_T = (iota_T --> bool_T) --> bool_T
 
 fun is_variable s = Char.isUpper (String.sub (s, 0))
 
 fun hol_term_from_fo_term res_T (ATerm (x, us)) =
-  let val ts = map (hol_term_from_fo_term iotaT) us in
+  let val ts = map (hol_term_from_fo_term iota_T) us in
     list_comb ((case x of
                   "$true" => @{const_name True}
                 | "$false" => @{const_name False}
@@ -82,8 +82,8 @@
     AQuant (_, [], phi') => hol_prop_from_formula phi'
   | AQuant (q, (x, _) :: xs, phi') =>
     Const (case q of AForall => @{const_name All} | AExists => @{const_name Ex},
-           quantT)
-    $ lambda (Free (x, iotaT)) (hol_prop_from_formula (AQuant (q, xs, phi')))
+           quant_T)
+    $ lambda (Free (x, iota_T)) (hol_prop_from_formula (AQuant (q, xs, phi')))
   | AConn (ANot, [u']) => HOLogic.mk_not (hol_prop_from_formula u')
   | AConn (c, [u1, u2]) =>
     pairself hol_prop_from_formula (u1, u2)
@@ -94,9 +94,9 @@
         | AIff => HOLogic.mk_eq
         | ANot => raise Fail "binary \"ANot\"")
   | AConn _ => raise Fail "malformed AConn"
-  | AAtom u => hol_term_from_fo_term boolT u
+  | AAtom u => hol_term_from_fo_term bool_T u
 
-fun mk_all x t = Const (@{const_name All}, quantT) $ lambda x t
+fun mk_all x t = Const (@{const_name All}, quant_T) $ lambda x t
 
 fun close_hol_prop t = fold (mk_all o Free) (Term.add_frees t []) t