1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jul 29 17:27:58 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Thu Jul 29 17:27:59 2010 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature CODE_PROLOG =
     1.6  sig
     1.7 -  datatype prol_term = Var of string * typ | Cons of string | AppF of string * prol_term list;
     1.8 +  datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list;
     1.9    datatype prem = Conj of prem list | NotRel of string * prol_term list
    1.10      | Rel of string * prol_term list | Eq of prol_term * prol_term | NotEq of prol_term * prol_term;
    1.11    type clause = ((string * prol_term list) * prem);
    1.12 @@ -35,9 +35,9 @@
    1.13  
    1.14  (* internal program representation *)
    1.15  
    1.16 -datatype prol_term = Var of string * typ | Cons of string | AppF of string * prol_term list;
    1.17 +datatype prol_term = Var of string | Cons of string | AppF of string * prol_term list;
    1.18  
    1.19 -fun string_of_prol_term (Var (s, T)) = "Var " ^ s
    1.20 +fun string_of_prol_term (Var s) = "Var " ^ s
    1.21    | string_of_prol_term (Cons s) = "Cons " ^ s
    1.22    | string_of_prol_term (AppF (f, args)) = f ^ "(" ^ commas (map string_of_prol_term args) ^ ")" 
    1.23  
    1.24 @@ -82,7 +82,7 @@
    1.25  
    1.26  fun translate_term ctxt constant_table t =
    1.27    case strip_comb t of
    1.28 -    (Free (v, T), []) => Var (v, T) 
    1.29 +    (Free (v, T), []) => Var v 
    1.30    | (Const (c, _), []) => Cons (translate_const constant_table c)
    1.31    | (Const (c, _), args) =>
    1.32      AppF (translate_const constant_table c, map (translate_term ctxt constant_table) args)
    1.33 @@ -142,8 +142,8 @@
    1.34  fun mk_groundness_prems ts =
    1.35    let
    1.36      val vars = fold add_vars ts []
    1.37 -    fun mk_ground (v, T) =
    1.38 -      Rel ("ground_" ^ string_of_typ T, [Var (v, T)])
    1.39 +    fun mk_ground v =
    1.40 +      Rel ("ground", [Var v])
    1.41    in
    1.42      map mk_ground vars
    1.43    end
    1.44 @@ -158,7 +158,7 @@
    1.45  
    1.46  (* code printer *)
    1.47  
    1.48 -fun write_term (Var (v, _)) = first_upper v
    1.49 +fun write_term (Var v) = first_upper v
    1.50    | write_term (Cons c) = c
    1.51    | write_term (AppF (f, args)) = f ^ "(" ^ space_implode ", " (map write_term args) ^ ")" 
    1.52  
    1.53 @@ -223,7 +223,7 @@
    1.54  fun scan_terms xs = (((scan_term --| $$ ",") ::: scan_terms)
    1.55    || (scan_term >> single)) xs
    1.56  and scan_term xs =
    1.57 -  ((scan_var >> (fn s => Var (string_of s, dummyT)))
    1.58 +  ((scan_var >> (Var o string_of))
    1.59    || ((scan_atom -- ($$ "(" |-- scan_terms --| $$ ")"))
    1.60      >> (fn (f, ts) => AppF (string_of f, ts)))
    1.61    || (scan_atom >> (Cons o string_of))) xs
    1.62 @@ -261,7 +261,7 @@
    1.63  
    1.64  (* values command *)
    1.65  
    1.66 -fun restore_term ctxt constant_table (Var (s, _), T) = Free (s, T)
    1.67 +fun restore_term ctxt constant_table (Var s, T) = Free (s, T)
    1.68    | restore_term ctxt constant_table (Cons s, T) = Const (restore_const constant_table s, T)
    1.69    | restore_term ctxt constant_table (AppF (f, args), T) =
    1.70      let