removed opening of structures
authorPhilipp Meyer
Tue Sep 22 14:17:54 2009 +0200 (2009-09-22)
changeset 32828ad76967c703d
parent 32827 2729c8033326
child 32829 671eb46eb0a3
removed opening of structures
src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML
src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
     1.1 --- a/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Thu Oct 01 18:59:26 2009 +0200
     1.2 +++ b/src/HOL/Library/Sum_Of_Squares/positivstellensatz_tools.ML	Tue Sep 22 14:17:54 2009 +0200
     1.3 @@ -16,8 +16,6 @@
     1.4  structure PositivstellensatzTools : POSITIVSTELLENSATZ_TOOLS =
     1.5  struct
     1.6  
     1.7 -open RealArith FuncUtil
     1.8 -
     1.9  (*** certificate generation ***)
    1.10  
    1.11  fun string_of_rat r =
    1.12 @@ -41,42 +39,42 @@
    1.13    end
    1.14  
    1.15  fun string_of_monomial m = 
    1.16 - if Ctermfunc.is_undefined m then "1" 
    1.17 + if FuncUtil.Ctermfunc.is_undefined m then "1" 
    1.18   else 
    1.19    let 
    1.20 -   val m' = dest_monomial m
    1.21 +   val m' = FuncUtil.dest_monomial m
    1.22     val vps = fold_rev (fn (x,k) => cons (string_of_varpow x k)) m' [] 
    1.23    in foldr1 (fn (s, t) => s ^ "*" ^ t) vps
    1.24    end
    1.25  
    1.26  fun string_of_cmonomial (m,c) =
    1.27 -  if Ctermfunc.is_undefined m then string_of_rat c
    1.28 +  if FuncUtil.Ctermfunc.is_undefined m then string_of_rat c
    1.29    else if c = Rat.one then string_of_monomial m
    1.30    else (string_of_rat c) ^ "*" ^ (string_of_monomial m);
    1.31  
    1.32  fun string_of_poly p = 
    1.33 - if Monomialfunc.is_undefined p then "0" 
    1.34 + if FuncUtil.Monomialfunc.is_undefined p then "0" 
    1.35   else
    1.36    let 
    1.37     val cms = map string_of_cmonomial
    1.38 -     (sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p))
    1.39 +     (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.graph p))
    1.40    in foldr1 (fn (t1, t2) => t1 ^ " + " ^ t2) cms
    1.41    end;
    1.42  
    1.43 -fun pss_to_cert (Axiom_eq i) = "A=" ^ string_of_int i
    1.44 -  | pss_to_cert (Axiom_le i) = "A<=" ^ string_of_int i
    1.45 -  | pss_to_cert (Axiom_lt i) = "A<" ^ string_of_int i
    1.46 -  | pss_to_cert (Rational_eq r) = "R=" ^ string_of_rat r
    1.47 -  | pss_to_cert (Rational_le r) = "R<=" ^ string_of_rat r
    1.48 -  | pss_to_cert (Rational_lt r) = "R<" ^ string_of_rat r
    1.49 -  | pss_to_cert (Square p) = "[" ^ string_of_poly p ^ "]^2"
    1.50 -  | pss_to_cert (Eqmul (p, pss)) = "([" ^ string_of_poly p ^ "] * " ^ pss_to_cert pss ^ ")"
    1.51 -  | pss_to_cert (Sum (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " + " ^ pss_to_cert pss2 ^ ")"
    1.52 -  | pss_to_cert (Product (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " * " ^ pss_to_cert pss2 ^ ")"
    1.53 +fun pss_to_cert (RealArith.Axiom_eq i) = "A=" ^ string_of_int i
    1.54 +  | pss_to_cert (RealArith.Axiom_le i) = "A<=" ^ string_of_int i
    1.55 +  | pss_to_cert (RealArith.Axiom_lt i) = "A<" ^ string_of_int i
    1.56 +  | pss_to_cert (RealArith.Rational_eq r) = "R=" ^ string_of_rat r
    1.57 +  | pss_to_cert (RealArith.Rational_le r) = "R<=" ^ string_of_rat r
    1.58 +  | pss_to_cert (RealArith.Rational_lt r) = "R<" ^ string_of_rat r
    1.59 +  | pss_to_cert (RealArith.Square p) = "[" ^ string_of_poly p ^ "]^2"
    1.60 +  | pss_to_cert (RealArith.Eqmul (p, pss)) = "([" ^ string_of_poly p ^ "] * " ^ pss_to_cert pss ^ ")"
    1.61 +  | pss_to_cert (RealArith.Sum (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " + " ^ pss_to_cert pss2 ^ ")"
    1.62 +  | pss_to_cert (RealArith.Product (pss1, pss2)) = "(" ^ pss_to_cert pss1 ^ " * " ^ pss_to_cert pss2 ^ ")"
    1.63  
    1.64 -fun pss_tree_to_cert Trivial = "()"
    1.65 -  | pss_tree_to_cert (Cert pss) = "(" ^ pss_to_cert pss ^ ")"
    1.66 -  | pss_tree_to_cert (Branch (t1, t2)) = "(" ^ pss_tree_to_cert t1 ^ " & " ^ pss_tree_to_cert t2 ^ ")"
    1.67 +fun pss_tree_to_cert RealArith.Trivial = "()"
    1.68 +  | pss_tree_to_cert (RealArith.Cert pss) = "(" ^ pss_to_cert pss ^ ")"
    1.69 +  | pss_tree_to_cert (RealArith.Branch (t1, t2)) = "(" ^ pss_tree_to_cert t1 ^ " & " ^ pss_tree_to_cert t2 ^ ")"
    1.70  
    1.71  (*** certificate parsing ***)
    1.72  
    1.73 @@ -103,27 +101,27 @@
    1.74    (fn (x, k) => (cterm_of (Context.theory_of_proof ctxt) (Free (x, @{typ real})), k)) 
    1.75  
    1.76  fun parse_monomial ctxt = repeat_sep "*" (parse_varpow ctxt) >>
    1.77 -  foldl (uncurry Ctermfunc.update) Ctermfunc.undefined
    1.78 +  foldl (uncurry FuncUtil.Ctermfunc.update) FuncUtil.Ctermfunc.undefined
    1.79  
    1.80  fun parse_cmonomial ctxt =
    1.81    rat_int --| str "*" -- (parse_monomial ctxt) >> swap ||
    1.82    (parse_monomial ctxt) >> (fn m => (m, Rat.one)) ||
    1.83 -  rat_int >> (fn r => (Ctermfunc.undefined, r))
    1.84 +  rat_int >> (fn r => (FuncUtil.Ctermfunc.undefined, r))
    1.85  
    1.86  fun parse_poly ctxt = repeat_sep "+" (parse_cmonomial ctxt) >>
    1.87 -  foldl (uncurry Monomialfunc.update) Monomialfunc.undefined
    1.88 +  foldl (uncurry FuncUtil.Monomialfunc.update) FuncUtil.Monomialfunc.undefined
    1.89  
    1.90  (* positivstellensatz parser *)
    1.91  
    1.92  val parse_axiom =
    1.93 -  (str "A=" |-- int >> Axiom_eq) ||
    1.94 -  (str "A<=" |-- int >> Axiom_le) ||
    1.95 -  (str "A<" |-- int >> Axiom_lt)
    1.96 +  (str "A=" |-- int >> RealArith.Axiom_eq) ||
    1.97 +  (str "A<=" |-- int >> RealArith.Axiom_le) ||
    1.98 +  (str "A<" |-- int >> RealArith.Axiom_lt)
    1.99  
   1.100  val parse_rational =
   1.101 -  (str "R=" |-- rat_int >> Rational_eq) ||
   1.102 -  (str "R<=" |-- rat_int >> Rational_le) ||
   1.103 -  (str "R<" |-- rat_int >> Rational_lt)
   1.104 +  (str "R=" |-- rat_int >> RealArith.Rational_eq) ||
   1.105 +  (str "R<=" |-- rat_int >> RealArith.Rational_le) ||
   1.106 +  (str "R<" |-- rat_int >> RealArith.Rational_lt)
   1.107  
   1.108  fun parse_cert ctxt input =
   1.109    let
   1.110 @@ -132,10 +130,10 @@
   1.111    in
   1.112    (parse_axiom ||
   1.113     parse_rational ||
   1.114 -   str "[" |-- pp --| str "]^2" >> Square ||
   1.115 -   str "([" |-- pp --| str "]*" -- pc --| str ")" >> Eqmul ||
   1.116 -   str "(" |-- pc --| str "*" -- pc --| str ")" >> Product ||
   1.117 -   str "(" |-- pc --| str "+" -- pc --| str ")" >> Sum) input
   1.118 +   str "[" |-- pp --| str "]^2" >> RealArith.Square ||
   1.119 +   str "([" |-- pp --| str "]*" -- pc --| str ")" >> RealArith.Eqmul ||
   1.120 +   str "(" |-- pc --| str "*" -- pc --| str ")" >> RealArith.Product ||
   1.121 +   str "(" |-- pc --| str "+" -- pc --| str ")" >> RealArith.Sum) input
   1.122    end
   1.123  
   1.124  fun parse_cert_tree ctxt input =
   1.125 @@ -143,9 +141,9 @@
   1.126      val pc = parse_cert ctxt
   1.127      val pt = parse_cert_tree ctxt
   1.128    in
   1.129 -  (str "()" >> K Trivial ||
   1.130 -   str "(" |-- pc --| str ")" >> Cert ||
   1.131 -   str "(" |-- pt --| str "&" -- pt --| str ")" >> Branch) input
   1.132 +  (str "()" >> K RealArith.Trivial ||
   1.133 +   str "(" |-- pc --| str ")" >> RealArith.Cert ||
   1.134 +   str "(" |-- pt --| str "&" -- pt --| str ")" >> RealArith.Branch) input
   1.135    end
   1.136  
   1.137  (* scanner *)
     2.1 --- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Thu Oct 01 18:59:26 2009 +0200
     2.2 +++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML	Tue Sep 22 14:17:54 2009 +0200
     2.3 @@ -23,8 +23,6 @@
     2.4  structure Sos : SOS = 
     2.5  struct
     2.6  
     2.7 -open FuncUtil;
     2.8 -
     2.9  val rat_0 = Rat.zero;
    2.10  val rat_1 = Rat.one;
    2.11  val rat_2 = Rat.two;
    2.12 @@ -104,9 +102,9 @@
    2.13  
    2.14  (* The main types.                                                           *)
    2.15  
    2.16 -type vector = int* Rat.rat Intfunc.T;
    2.17 +type vector = int* Rat.rat FuncUtil.Intfunc.T;
    2.18  
    2.19 -type matrix = (int*int)*(Rat.rat Intpairfunc.T);
    2.20 +type matrix = (int*int)*(Rat.rat FuncUtil.Intpairfunc.T);
    2.21  
    2.22  fun iszero (k,r) = r =/ rat_0;
    2.23  
    2.24 @@ -118,29 +116,29 @@
    2.25   
    2.26  (* Vectors. Conventionally indexed 1..n.                                     *)
    2.27  
    2.28 -fun vector_0 n = (n,Intfunc.undefined):vector;
    2.29 +fun vector_0 n = (n,FuncUtil.Intfunc.undefined):vector;
    2.30  
    2.31  fun dim (v:vector) = fst v;
    2.32  
    2.33  fun vector_const c n =
    2.34    if c =/ rat_0 then vector_0 n
    2.35 -  else (n,fold_rev (fn k => Intfunc.update (k,c)) (1 upto n) Intfunc.undefined) :vector;
    2.36 +  else (n,fold_rev (fn k => FuncUtil.Intfunc.update (k,c)) (1 upto n) FuncUtil.Intfunc.undefined) :vector;
    2.37  
    2.38  val vector_1 = vector_const rat_1;
    2.39  
    2.40  fun vector_cmul c (v:vector) =
    2.41   let val n = dim v 
    2.42   in if c =/ rat_0 then vector_0 n
    2.43 -    else (n,Intfunc.mapf (fn x => c */ x) (snd v))
    2.44 +    else (n,FuncUtil.Intfunc.mapf (fn x => c */ x) (snd v))
    2.45   end;
    2.46  
    2.47 -fun vector_neg (v:vector) = (fst v,Intfunc.mapf Rat.neg (snd v)) :vector;
    2.48 +fun vector_neg (v:vector) = (fst v,FuncUtil.Intfunc.mapf Rat.neg (snd v)) :vector;
    2.49  
    2.50  fun vector_add (v1:vector) (v2:vector) =
    2.51   let val m = dim v1  
    2.52       val n = dim v2 
    2.53   in if m <> n then error "vector_add: incompatible dimensions"
    2.54 -    else (n,Intfunc.combine (curry op +/) (fn x => x =/ rat_0) (snd v1) (snd v2)) :vector 
    2.55 +    else (n,FuncUtil.Intfunc.combine (curry op +/) (fn x => x =/ rat_0) (snd v1) (snd v2)) :vector 
    2.56   end;
    2.57  
    2.58  fun vector_sub v1 v2 = vector_add v1 (vector_neg v2);
    2.59 @@ -149,43 +147,43 @@
    2.60   let val m = dim v1 
    2.61       val n = dim v2 
    2.62   in if m <> n then error "vector_dot: incompatible dimensions" 
    2.63 -    else Intfunc.fold (fn (i,x) => fn a => x +/ a) 
    2.64 -        (Intfunc.combine (curry op */) (fn x => x =/ rat_0) (snd v1) (snd v2)) rat_0
    2.65 +    else FuncUtil.Intfunc.fold (fn (i,x) => fn a => x +/ a) 
    2.66 +        (FuncUtil.Intfunc.combine (curry op */) (fn x => x =/ rat_0) (snd v1) (snd v2)) rat_0
    2.67   end;
    2.68  
    2.69  fun vector_of_list l =
    2.70   let val n = length l 
    2.71 - in (n,fold_rev2 (curry Intfunc.update) (1 upto n) l Intfunc.undefined) :vector
    2.72 + in (n,fold_rev2 (curry FuncUtil.Intfunc.update) (1 upto n) l FuncUtil.Intfunc.undefined) :vector
    2.73   end;
    2.74  
    2.75  (* Matrices; again rows and columns indexed from 1.                          *)
    2.76  
    2.77 -fun matrix_0 (m,n) = ((m,n),Intpairfunc.undefined):matrix;
    2.78 +fun matrix_0 (m,n) = ((m,n),FuncUtil.Intpairfunc.undefined):matrix;
    2.79  
    2.80  fun dimensions (m:matrix) = fst m;
    2.81  
    2.82  fun matrix_const c (mn as (m,n)) =
    2.83    if m <> n then error "matrix_const: needs to be square"
    2.84    else if c =/ rat_0 then matrix_0 mn
    2.85 -  else (mn,fold_rev (fn k => Intpairfunc.update ((k,k), c)) (1 upto n) Intpairfunc.undefined) :matrix;;
    2.86 +  else (mn,fold_rev (fn k => FuncUtil.Intpairfunc.update ((k,k), c)) (1 upto n) FuncUtil.Intpairfunc.undefined) :matrix;;
    2.87  
    2.88  val matrix_1 = matrix_const rat_1;
    2.89  
    2.90  fun matrix_cmul c (m:matrix) =
    2.91   let val (i,j) = dimensions m 
    2.92   in if c =/ rat_0 then matrix_0 (i,j)
    2.93 -    else ((i,j),Intpairfunc.mapf (fn x => c */ x) (snd m))
    2.94 +    else ((i,j),FuncUtil.Intpairfunc.mapf (fn x => c */ x) (snd m))
    2.95   end;
    2.96  
    2.97  fun matrix_neg (m:matrix) = 
    2.98 -  (dimensions m, Intpairfunc.mapf Rat.neg (snd m)) :matrix;
    2.99 +  (dimensions m, FuncUtil.Intpairfunc.mapf Rat.neg (snd m)) :matrix;
   2.100  
   2.101  fun matrix_add (m1:matrix) (m2:matrix) =
   2.102   let val d1 = dimensions m1 
   2.103       val d2 = dimensions m2 
   2.104   in if d1 <> d2 
   2.105       then error "matrix_add: incompatible dimensions"
   2.106 -    else (d1,Intpairfunc.combine (curry op +/) (fn x => x =/ rat_0) (snd m1) (snd m2)) :matrix
   2.107 +    else (d1,FuncUtil.Intpairfunc.combine (curry op +/) (fn x => x =/ rat_0) (snd m1) (snd m2)) :matrix
   2.108   end;;
   2.109  
   2.110  fun matrix_sub m1 m2 = matrix_add m1 (matrix_neg m2);
   2.111 @@ -193,112 +191,112 @@
   2.112  fun row k (m:matrix) =
   2.113   let val (i,j) = dimensions m 
   2.114   in (j,
   2.115 -   Intpairfunc.fold (fn ((i,j), c) => fn a => if i = k then Intfunc.update (j,c) a else a) (snd m) Intfunc.undefined ) : vector
   2.116 +   FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn a => if i = k then FuncUtil.Intfunc.update (j,c) a else a) (snd m) FuncUtil.Intfunc.undefined ) : vector
   2.117   end;
   2.118  
   2.119  fun column k (m:matrix) =
   2.120    let val (i,j) = dimensions m 
   2.121    in (i,
   2.122 -   Intpairfunc.fold (fn ((i,j), c) => fn a => if j = k then Intfunc.update (i,c) a else a) (snd m)  Intfunc.undefined)
   2.123 +   FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn a => if j = k then FuncUtil.Intfunc.update (i,c) a else a) (snd m)  FuncUtil.Intfunc.undefined)
   2.124     : vector
   2.125   end;
   2.126  
   2.127  fun transp (m:matrix) =
   2.128    let val (i,j) = dimensions m 
   2.129    in
   2.130 -  ((j,i),Intpairfunc.fold (fn ((i,j), c) => fn a => Intpairfunc.update ((j,i), c) a) (snd m) Intpairfunc.undefined) :matrix
   2.131 +  ((j,i),FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn a => FuncUtil.Intpairfunc.update ((j,i), c) a) (snd m) FuncUtil.Intpairfunc.undefined) :matrix
   2.132   end;
   2.133  
   2.134  fun diagonal (v:vector) =
   2.135   let val n = dim v 
   2.136 - in ((n,n),Intfunc.fold (fn (i, c) => fn a => Intpairfunc.update ((i,i), c) a) (snd v) Intpairfunc.undefined) : matrix
   2.137 + in ((n,n),FuncUtil.Intfunc.fold (fn (i, c) => fn a => FuncUtil.Intpairfunc.update ((i,i), c) a) (snd v) FuncUtil.Intpairfunc.undefined) : matrix
   2.138   end;
   2.139  
   2.140  fun matrix_of_list l =
   2.141   let val m = length l 
   2.142   in if m = 0 then matrix_0 (0,0) else
   2.143     let val n = length (hd l) 
   2.144 -   in ((m,n),itern 1 l (fn v => fn i => itern 1 v (fn c => fn j => Intpairfunc.update ((i,j), c))) Intpairfunc.undefined)
   2.145 +   in ((m,n),itern 1 l (fn v => fn i => itern 1 v (fn c => fn j => FuncUtil.Intpairfunc.update ((i,j), c))) FuncUtil.Intpairfunc.undefined)
   2.146     end
   2.147   end;
   2.148  
   2.149  (* Monomials.                                                                *)
   2.150  
   2.151 -fun monomial_eval assig (m:monomial) =
   2.152 -  Ctermfunc.fold (fn (x, k) => fn a => a */ rat_pow (Ctermfunc.apply assig x) k)
   2.153 +fun monomial_eval assig m =
   2.154 +  FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => a */ rat_pow (FuncUtil.Ctermfunc.apply assig x) k)
   2.155          m rat_1;
   2.156 -val monomial_1 = (Ctermfunc.undefined:monomial);
   2.157 +val monomial_1 = FuncUtil.Ctermfunc.undefined;
   2.158  
   2.159 -fun monomial_var x = Ctermfunc.onefunc (x, 1) :monomial;
   2.160 +fun monomial_var x = FuncUtil.Ctermfunc.onefunc (x, 1);
   2.161  
   2.162 -val (monomial_mul:monomial->monomial->monomial) =
   2.163 -  Ctermfunc.combine (curry op +) (K false);
   2.164 +val monomial_mul =
   2.165 +  FuncUtil.Ctermfunc.combine (curry op +) (K false);
   2.166  
   2.167 -fun monomial_pow (m:monomial) k =
   2.168 +fun monomial_pow m k =
   2.169    if k = 0 then monomial_1
   2.170 -  else Ctermfunc.mapf (fn x => k * x) m;
   2.171 +  else FuncUtil.Ctermfunc.mapf (fn x => k * x) m;
   2.172  
   2.173 -fun monomial_divides (m1:monomial) (m2:monomial) =
   2.174 -  Ctermfunc.fold (fn (x, k) => fn a => Ctermfunc.tryapplyd m2 x 0 >= k andalso a) m1 true;;
   2.175 +fun monomial_divides m1 m2 =
   2.176 +  FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => FuncUtil.Ctermfunc.tryapplyd m2 x 0 >= k andalso a) m1 true;;
   2.177  
   2.178 -fun monomial_div (m1:monomial) (m2:monomial) =
   2.179 - let val m = Ctermfunc.combine (curry op +) 
   2.180 -   (fn x => x = 0) m1 (Ctermfunc.mapf (fn x => ~ x) m2) 
   2.181 - in if Ctermfunc.fold (fn (x, k) => fn a => k >= 0 andalso a) m true then m
   2.182 +fun monomial_div m1 m2 =
   2.183 + let val m = FuncUtil.Ctermfunc.combine (curry op +) 
   2.184 +   (fn x => x = 0) m1 (FuncUtil.Ctermfunc.mapf (fn x => ~ x) m2) 
   2.185 + in if FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k >= 0 andalso a) m true then m
   2.186    else error "monomial_div: non-divisible"
   2.187   end;
   2.188  
   2.189 -fun monomial_degree x (m:monomial) = 
   2.190 -  Ctermfunc.tryapplyd m x 0;;
   2.191 +fun monomial_degree x m = 
   2.192 +  FuncUtil.Ctermfunc.tryapplyd m x 0;;
   2.193  
   2.194 -fun monomial_lcm (m1:monomial) (m2:monomial) =
   2.195 -  fold_rev (fn x => Ctermfunc.update (x, max (monomial_degree x m1) (monomial_degree x m2)))
   2.196 -          (gen_union (is_equal o  cterm_ord) (Ctermfunc.dom m1, Ctermfunc.dom m2)) (Ctermfunc.undefined :monomial);
   2.197 +fun monomial_lcm m1 m2 =
   2.198 +  fold_rev (fn x => FuncUtil.Ctermfunc.update (x, max (monomial_degree x m1) (monomial_degree x m2)))
   2.199 +          (gen_union (is_equal o  FuncUtil.cterm_ord) (FuncUtil.Ctermfunc.dom m1, FuncUtil.Ctermfunc.dom m2)) (FuncUtil.Ctermfunc.undefined);
   2.200  
   2.201 -fun monomial_multidegree (m:monomial) = 
   2.202 - Ctermfunc.fold (fn (x, k) => fn a => k + a) m 0;;
   2.203 +fun monomial_multidegree m = 
   2.204 + FuncUtil.Ctermfunc.fold (fn (x, k) => fn a => k + a) m 0;;
   2.205  
   2.206 -fun monomial_variables m = Ctermfunc.dom m;;
   2.207 +fun monomial_variables m = FuncUtil.Ctermfunc.dom m;;
   2.208  
   2.209  (* Polynomials.                                                              *)
   2.210  
   2.211 -fun eval assig (p:poly) =
   2.212 -  Monomialfunc.fold (fn (m, c) => fn a => a +/ c */ monomial_eval assig m) p rat_0;
   2.213 +fun eval assig p =
   2.214 +  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => a +/ c */ monomial_eval assig m) p rat_0;
   2.215  
   2.216 -val poly_0 = (Monomialfunc.undefined:poly);
   2.217 +val poly_0 = FuncUtil.Monomialfunc.undefined;
   2.218  
   2.219 -fun poly_isconst (p:poly) = 
   2.220 -  Monomialfunc.fold (fn (m, c) => fn a => Ctermfunc.is_undefined m andalso a) p true;
   2.221 +fun poly_isconst p = 
   2.222 +  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => FuncUtil.Ctermfunc.is_undefined m andalso a) p true;
   2.223  
   2.224 -fun poly_var x = Monomialfunc.onefunc (monomial_var x,rat_1) :poly;
   2.225 +fun poly_var x = FuncUtil.Monomialfunc.onefunc (monomial_var x,rat_1);
   2.226  
   2.227  fun poly_const c =
   2.228 -  if c =/ rat_0 then poly_0 else Monomialfunc.onefunc(monomial_1, c);
   2.229 +  if c =/ rat_0 then poly_0 else FuncUtil.Monomialfunc.onefunc(monomial_1, c);
   2.230  
   2.231 -fun poly_cmul c (p:poly) =
   2.232 +fun poly_cmul c p =
   2.233    if c =/ rat_0 then poly_0
   2.234 -  else Monomialfunc.mapf (fn x => c */ x) p;
   2.235 +  else FuncUtil.Monomialfunc.mapf (fn x => c */ x) p;
   2.236  
   2.237 -fun poly_neg (p:poly) = (Monomialfunc.mapf Rat.neg p :poly);;
   2.238 +fun poly_neg p = FuncUtil.Monomialfunc.mapf Rat.neg p;;
   2.239  
   2.240 -fun poly_add (p1:poly) (p2:poly) =
   2.241 -  (Monomialfunc.combine (curry op +/) (fn x => x =/ rat_0) p1 p2 :poly);
   2.242 +fun poly_add p1 p2 =
   2.243 +  FuncUtil.Monomialfunc.combine (curry op +/) (fn x => x =/ rat_0) p1 p2;
   2.244  
   2.245  fun poly_sub p1 p2 = poly_add p1 (poly_neg p2);
   2.246  
   2.247 -fun poly_cmmul (c,m) (p:poly) =
   2.248 +fun poly_cmmul (c,m) p =
   2.249   if c =/ rat_0 then poly_0
   2.250 - else if Ctermfunc.is_undefined m 
   2.251 -      then Monomialfunc.mapf (fn d => c */ d) p
   2.252 -      else Monomialfunc.fold (fn (m', d) => fn a => (Monomialfunc.update (monomial_mul m m', c */ d) a)) p poly_0;
   2.253 + else if FuncUtil.Ctermfunc.is_undefined m 
   2.254 +      then FuncUtil.Monomialfunc.mapf (fn d => c */ d) p
   2.255 +      else FuncUtil.Monomialfunc.fold (fn (m', d) => fn a => (FuncUtil.Monomialfunc.update (monomial_mul m m', c */ d) a)) p poly_0;
   2.256  
   2.257 -fun poly_mul (p1:poly) (p2:poly) =
   2.258 -  Monomialfunc.fold (fn (m, c) => fn a => poly_add (poly_cmmul (c,m) p2) a) p1 poly_0;
   2.259 +fun poly_mul p1 p2 =
   2.260 +  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => poly_add (poly_cmmul (c,m) p2) a) p1 poly_0;
   2.261  
   2.262 -fun poly_div (p1:poly) (p2:poly) =
   2.263 +fun poly_div p1 p2 =
   2.264   if not(poly_isconst p2) 
   2.265   then error "poly_div: non-constant" else
   2.266 - let val c = eval Ctermfunc.undefined p2 
   2.267 + let val c = eval FuncUtil.Ctermfunc.undefined p2 
   2.268   in if c =/ rat_0 then error "poly_div: division by zero"
   2.269      else poly_cmul (Rat.inv c) p1
   2.270   end;
   2.271 @@ -314,22 +312,20 @@
   2.272  fun poly_exp p1 p2 =
   2.273    if not(poly_isconst p2) 
   2.274    then error "poly_exp: not a constant" 
   2.275 -  else poly_pow p1 (int_of_rat (eval Ctermfunc.undefined p2));
   2.276 +  else poly_pow p1 (int_of_rat (eval FuncUtil.Ctermfunc.undefined p2));
   2.277  
   2.278 -fun degree x (p:poly) = 
   2.279 - Monomialfunc.fold (fn (m,c) => fn a => max (monomial_degree x m) a) p 0;
   2.280 +fun degree x p = 
   2.281 + FuncUtil.Monomialfunc.fold (fn (m,c) => fn a => max (monomial_degree x m) a) p 0;
   2.282  
   2.283 -fun multidegree (p:poly) =
   2.284 -  Monomialfunc.fold (fn (m, c) => fn a => max (monomial_multidegree m) a) p 0;
   2.285 +fun multidegree p =
   2.286 +  FuncUtil.Monomialfunc.fold (fn (m, c) => fn a => max (monomial_multidegree m) a) p 0;
   2.287  
   2.288 -fun poly_variables (p:poly) =
   2.289 -  sort cterm_ord (Monomialfunc.fold_rev (fn (m, c) => curry (gen_union (is_equal o  cterm_ord)) (monomial_variables m)) p []);;
   2.290 +fun poly_variables p =
   2.291 +  sort FuncUtil.cterm_ord (FuncUtil.Monomialfunc.fold_rev (fn (m, c) => curry (gen_union (is_equal o  FuncUtil.cterm_ord)) (monomial_variables m)) p []);;
   2.292  
   2.293  (* Order monomials for human presentation.                                   *)
   2.294  
   2.295 -fun cterm_ord (t,t') = TermOrd.fast_term_ord (term_of t, term_of t');
   2.296 -
   2.297 -val humanorder_varpow = prod_ord cterm_ord (rev_order o int_ord);
   2.298 +val humanorder_varpow = prod_ord FuncUtil.cterm_ord (rev_order o int_ord);
   2.299  
   2.300  local
   2.301   fun ord (l1,l2) = case (l1,l2) of
   2.302 @@ -341,8 +337,8 @@
   2.303     | EQUAL => ord (t1,t2)
   2.304     | GREATER => GREATER)
   2.305  in fun humanorder_monomial m1 m2 = 
   2.306 - ord (sort humanorder_varpow (Ctermfunc.graph m1),
   2.307 -  sort humanorder_varpow (Ctermfunc.graph m2))
   2.308 + ord (sort humanorder_varpow (FuncUtil.Ctermfunc.graph m1),
   2.309 +  sort humanorder_varpow (FuncUtil.Ctermfunc.graph m2))
   2.310  end;
   2.311  
   2.312  (* Conversions to strings.                                                   *)
   2.313 @@ -352,7 +348,7 @@
   2.314   in if n_raw = 0 then "[]" else
   2.315    let 
   2.316     val n = max min_size (min n_raw max_size) 
   2.317 -   val xs = map (Rat.string_of_rat o (fn i => Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
   2.318 +   val xs = map (Rat.string_of_rat o (fn i => FuncUtil.Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
   2.319    in "[" ^ foldr1 (fn (s, t) => s ^ ", " ^ t) xs ^
   2.320    (if n_raw > max_size then ", ...]" else "]")
   2.321    end
   2.322 @@ -387,21 +383,21 @@
   2.323    else string_of_cterm x^"^"^string_of_int k;
   2.324  
   2.325  fun string_of_monomial m =
   2.326 - if Ctermfunc.is_undefined m then "1" else
   2.327 + if FuncUtil.Ctermfunc.is_undefined m then "1" else
   2.328   let val vps = fold_rev (fn (x,k) => fn a => string_of_varpow x k :: a)
   2.329 -  (sort humanorder_varpow (Ctermfunc.graph m)) [] 
   2.330 +  (sort humanorder_varpow (FuncUtil.Ctermfunc.graph m)) [] 
   2.331   in foldr1 (fn (s, t) => s^"*"^t) vps
   2.332   end;
   2.333  
   2.334  fun string_of_cmonomial (c,m) =
   2.335 - if Ctermfunc.is_undefined m then Rat.string_of_rat c
   2.336 + if FuncUtil.Ctermfunc.is_undefined m then Rat.string_of_rat c
   2.337   else if c =/ rat_1 then string_of_monomial m
   2.338   else Rat.string_of_rat c ^ "*" ^ string_of_monomial m;;
   2.339  
   2.340  fun string_of_poly p =
   2.341 - if Monomialfunc.is_undefined p then "<<0>>" else
   2.342 + if FuncUtil.Monomialfunc.is_undefined p then "<<0>>" else
   2.343   let 
   2.344 -  val cms = sort (fn ((m1,_),(m2,_)) => humanorder_monomial m1  m2) (Monomialfunc.graph p)
   2.345 +  val cms = sort (fn ((m1,_),(m2,_)) => humanorder_monomial m1  m2) (FuncUtil.Monomialfunc.graph p)
   2.346    val s = fold (fn (m,c) => fn a =>
   2.347               if c </ rat_0 then a ^ " - " ^ string_of_cmonomial(Rat.neg c,m)
   2.348               else a ^ " + " ^ string_of_cmonomial(c,m))
   2.349 @@ -434,7 +430,7 @@
   2.350        else if lop aconvc inv_tm then
   2.351         let val p = poly_of_term r 
   2.352         in if poly_isconst p 
   2.353 -          then poly_const(Rat.inv (eval Ctermfunc.undefined p))
   2.354 +          then poly_const(Rat.inv (eval FuncUtil.Ctermfunc.undefined p))
   2.355            else error "poly_of_term: inverse of non-constant polyomial"
   2.356         end
   2.357     else (let val (opr,l) = Thm.dest_comb lop
   2.358 @@ -451,7 +447,7 @@
   2.359             then let 
   2.360                    val p = poly_of_term l 
   2.361                    val q = poly_of_term r 
   2.362 -                in if poly_isconst q then poly_cmul (Rat.inv (eval Ctermfunc.undefined q)) p
   2.363 +                in if poly_isconst q then poly_cmul (Rat.inv (eval FuncUtil.Ctermfunc.undefined q)) p
   2.364                     else error "poly_of_term: division by non-constant polynomial"
   2.365                  end
   2.366            else poly_var tm
   2.367 @@ -471,7 +467,7 @@
   2.368  fun sdpa_of_vector (v:vector) =
   2.369   let 
   2.370    val n = dim v
   2.371 -  val strs = map (decimalize 20 o (fn i => Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
   2.372 +  val strs = map (decimalize 20 o (fn i => FuncUtil.Intfunc.tryapplyd (snd v) i rat_0)) (1 upto n) 
   2.373   in foldr1 (fn (x, y) => x ^ " " ^ y) strs ^ "\n"
   2.374   end;
   2.375  
   2.376 @@ -487,7 +483,7 @@
   2.377    val pfx = string_of_int k ^" "
   2.378    val ents =
   2.379      Inttriplefunc.fold (fn ((b,i,j), c) => fn a => if i > j then a else ((b,i,j),c)::a) m []
   2.380 -  val entss = sort (increasing fst triple_int_ord ) ents
   2.381 +  val entss = sort (FuncUtil.increasing fst triple_int_ord ) ents
   2.382   in  fold_rev (fn ((b,i,j),c) => fn a =>
   2.383       pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^
   2.384       " " ^ decimalize 20 c ^ "\n" ^ a) entss ""
   2.385 @@ -498,8 +494,8 @@
   2.386  fun sdpa_of_matrix k (m:matrix) =
   2.387   let 
   2.388    val pfx = string_of_int k ^ " 1 "
   2.389 -  val ms = Intpairfunc.fold (fn ((i,j), c) => fn  a => if i > j then a else ((i,j),c)::a) (snd m) [] 
   2.390 -  val mss = sort (increasing fst (prod_ord int_ord int_ord)) ms 
   2.391 +  val ms = FuncUtil.Intpairfunc.fold (fn ((i,j), c) => fn  a => if i > j then a else ((i,j),c)::a) (snd m) [] 
   2.392 +  val mss = sort (FuncUtil.increasing fst (prod_ord int_ord int_ord)) ms 
   2.393   in fold_rev (fn ((i,j),c) => fn a =>
   2.394       pfx ^ string_of_int i ^ " " ^ string_of_int j ^
   2.395       " " ^ decimalize 20 c ^ "\n" ^ a) mss ""
   2.396 @@ -544,18 +540,15 @@
   2.397  
   2.398  (* More parser basics.                                                       *)
   2.399  
   2.400 -local
   2.401 - open Scan
   2.402 -in 
   2.403 - val word = this_string
   2.404 + val word = Scan.this_string
   2.405   fun token s =
   2.406 -  repeat ($$ " ") |-- word s --| repeat ($$ " ")
   2.407 - val numeral = one isnum
   2.408 - val decimalint = bulk numeral >> (rat_of_string o implode)
   2.409 - val decimalfrac = bulk numeral
   2.410 +  Scan.repeat ($$ " ") |-- word s --| Scan.repeat ($$ " ")
   2.411 + val numeral = Scan.one isnum
   2.412 + val decimalint = Scan.bulk numeral >> (rat_of_string o implode)
   2.413 + val decimalfrac = Scan.bulk numeral
   2.414      >> (fn s => rat_of_string(implode s) // pow10 (length s))
   2.415   val decimalsig =
   2.416 -    decimalint -- option (Scan.$$ "." |-- decimalfrac)
   2.417 +    decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)
   2.418      >> (fn (h,NONE) => h | (h,SOME x) => h +/ x)
   2.419   fun signed prs =
   2.420         $$ "-" |-- prs >> Rat.neg 
   2.421 @@ -568,7 +561,6 @@
   2.422  
   2.423   val decimal = signed decimalsig -- (emptyin rat_0|| exponent)
   2.424      >> (fn (h, x) => h */ pow10 (int_of_rat x));
   2.425 -end;
   2.426  
   2.427   fun mkparser p s =
   2.428    let val (x,rst) = p (explode s) 
   2.429 @@ -605,15 +597,15 @@
   2.430  
   2.431  fun pi_scale_then solver (obj:vector)  mats =
   2.432   let 
   2.433 -  val cd1 = fold_rev (common_denominator Intpairfunc.fold) mats (rat_1)
   2.434 -  val cd2 = common_denominator Intfunc.fold (snd obj)  (rat_1) 
   2.435 -  val mats' = map (Intpairfunc.mapf (fn x => cd1 */ x)) mats
   2.436 +  val cd1 = fold_rev (common_denominator FuncUtil.Intpairfunc.fold) mats (rat_1)
   2.437 +  val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj)  (rat_1) 
   2.438 +  val mats' = map (FuncUtil.Intpairfunc.mapf (fn x => cd1 */ x)) mats
   2.439    val obj' = vector_cmul cd2 obj
   2.440 -  val max1 = fold_rev (maximal_element Intpairfunc.fold) mats' (rat_0)
   2.441 -  val max2 = maximal_element Intfunc.fold (snd obj') (rat_0) 
   2.442 +  val max1 = fold_rev (maximal_element FuncUtil.Intpairfunc.fold) mats' (rat_0)
   2.443 +  val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0) 
   2.444    val scal1 = pow2 (20 - trunc(Math.ln (float_of_rat max1) / Math.ln 2.0))
   2.445    val scal2 = pow2 (20 - trunc(Math.ln (float_of_rat max2) / Math.ln 2.0)) 
   2.446 -  val mats'' = map (Intpairfunc.mapf (fn x => x */ scal1)) mats'
   2.447 +  val mats'' = map (FuncUtil.Intpairfunc.mapf (fn x => x */ scal1)) mats'
   2.448    val obj'' = vector_cmul scal2 obj' 
   2.449   in solver obj'' mats''
   2.450    end
   2.451 @@ -639,11 +631,11 @@
   2.452  fun tri_scale_then solver (obj:vector)  mats =
   2.453   let 
   2.454    val cd1 = fold_rev (common_denominator Inttriplefunc.fold) mats (rat_1)
   2.455 -  val cd2 = common_denominator Intfunc.fold (snd obj)  (rat_1) 
   2.456 +  val cd2 = common_denominator FuncUtil.Intfunc.fold (snd obj)  (rat_1) 
   2.457    val mats' = map (Inttriplefunc.mapf (fn x => cd1 */ x)) mats
   2.458    val obj' = vector_cmul cd2 obj
   2.459    val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' (rat_0)
   2.460 -  val max2 = maximal_element Intfunc.fold (snd obj') (rat_0) 
   2.461 +  val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') (rat_0) 
   2.462    val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
   2.463    val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0)) 
   2.464    val mats'' = map (Inttriplefunc.mapf (fn x => x */ scal1)) mats'
   2.465 @@ -656,10 +648,10 @@
   2.466  
   2.467  fun nice_rational n x = round_rat (n */ x) // n;;
   2.468  fun nice_vector n ((d,v) : vector) = 
   2.469 - (d, Intfunc.fold (fn (i,c) => fn a => 
   2.470 + (d, FuncUtil.Intfunc.fold (fn (i,c) => fn a => 
   2.471     let val y = nice_rational n c 
   2.472     in if c =/ rat_0 then a 
   2.473 -      else Intfunc.update (i,y) a end) v Intfunc.undefined):vector
   2.474 +      else FuncUtil.Intfunc.update (i,y) a end) v FuncUtil.Intfunc.undefined):vector
   2.475  
   2.476  fun dest_ord f x = is_equal (f x);
   2.477  
   2.478 @@ -763,11 +755,11 @@
   2.479  (* Multiply equation-parametrized poly by regular poly and add accumulator.  *)
   2.480  
   2.481  fun tri_epoly_pmul p q acc =
   2.482 - Monomialfunc.fold (fn (m1, c) => fn a =>
   2.483 -  Monomialfunc.fold (fn (m2,e) => fn b =>
   2.484 + FuncUtil.Monomialfunc.fold (fn (m1, c) => fn a =>
   2.485 +  FuncUtil.Monomialfunc.fold (fn (m2,e) => fn b =>
   2.486     let val m =  monomial_mul m1 m2
   2.487 -       val es = Monomialfunc.tryapplyd b m Inttriplefunc.undefined 
   2.488 -   in Monomialfunc.update (m,tri_equation_add (tri_equation_cmul c e) es) b 
   2.489 +       val es = FuncUtil.Monomialfunc.tryapplyd b m Inttriplefunc.undefined 
   2.490 +   in FuncUtil.Monomialfunc.update (m,tri_equation_add (tri_equation_cmul c e) es) b 
   2.491     end) q a) p acc ;
   2.492  
   2.493  (* Usual operations on equation-parametrized poly.                           *)
   2.494 @@ -881,11 +873,11 @@
   2.495  (* Multiply equation-parametrized poly by regular poly and add accumulator.  *)
   2.496  
   2.497  fun pi_epoly_pmul p q acc =
   2.498 - Monomialfunc.fold (fn (m1, c) => fn a =>
   2.499 -  Monomialfunc.fold (fn (m2,e) => fn b =>
   2.500 + FuncUtil.Monomialfunc.fold (fn (m1, c) => fn a =>
   2.501 +  FuncUtil.Monomialfunc.fold (fn (m2,e) => fn b =>
   2.502     let val m =  monomial_mul m1 m2
   2.503 -       val es = Monomialfunc.tryapplyd b m Inttriplefunc.undefined 
   2.504 -   in Monomialfunc.update (m,pi_equation_add (pi_equation_cmul c e) es) b 
   2.505 +       val es = FuncUtil.Monomialfunc.tryapplyd b m Inttriplefunc.undefined 
   2.506 +   in FuncUtil.Monomialfunc.update (m,pi_equation_add (pi_equation_cmul c e) es) b 
   2.507     end) q a) p acc ;
   2.508  
   2.509  (* Usual operations on equation-parametrized poly.                           *)
   2.510 @@ -914,27 +906,27 @@
   2.511  
   2.512  local
   2.513  fun diagonalize n i m =
   2.514 - if Intpairfunc.is_undefined (snd m) then [] 
   2.515 + if FuncUtil.Intpairfunc.is_undefined (snd m) then [] 
   2.516   else
   2.517 -  let val a11 = Intpairfunc.tryapplyd (snd m) (i,i) rat_0 
   2.518 +  let val a11 = FuncUtil.Intpairfunc.tryapplyd (snd m) (i,i) rat_0 
   2.519    in if a11 </ rat_0 then raise Failure "diagonalize: not PSD"
   2.520      else if a11 =/ rat_0 then
   2.521 -          if Intfunc.is_undefined (snd (row i m)) then diagonalize n (i + 1) m
   2.522 +          if FuncUtil.Intfunc.is_undefined (snd (row i m)) then diagonalize n (i + 1) m
   2.523            else raise Failure "diagonalize: not PSD ___ "
   2.524      else
   2.525       let 
   2.526        val v = row i m
   2.527 -      val v' = (fst v, Intfunc.fold (fn (i, c) => fn a => 
   2.528 +      val v' = (fst v, FuncUtil.Intfunc.fold (fn (i, c) => fn a => 
   2.529         let val y = c // a11 
   2.530 -       in if y = rat_0 then a else Intfunc.update (i,y) a 
   2.531 -       end)  (snd v) Intfunc.undefined)
   2.532 -      fun upt0 x y a = if y = rat_0 then a else Intpairfunc.update (x,y) a
   2.533 +       in if y = rat_0 then a else FuncUtil.Intfunc.update (i,y) a 
   2.534 +       end)  (snd v) FuncUtil.Intfunc.undefined)
   2.535 +      fun upt0 x y a = if y = rat_0 then a else FuncUtil.Intpairfunc.update (x,y) a
   2.536        val m' =
   2.537        ((n,n),
   2.538        iter (i+1,n) (fn j =>
   2.539            iter (i+1,n) (fn k =>
   2.540 -              (upt0 (j,k) (Intpairfunc.tryapplyd (snd m) (j,k) rat_0 -/ Intfunc.tryapplyd (snd v) j rat_0 */ Intfunc.tryapplyd (snd v') k rat_0))))
   2.541 -          Intpairfunc.undefined)
   2.542 +              (upt0 (j,k) (FuncUtil.Intpairfunc.tryapplyd (snd m) (j,k) rat_0 -/ FuncUtil.Intfunc.tryapplyd (snd v) j rat_0 */ FuncUtil.Intfunc.tryapplyd (snd v') k rat_0))))
   2.543 +          FuncUtil.Intpairfunc.undefined)
   2.544       in (a11,v')::diagonalize n (i + 1) m' 
   2.545       end
   2.546    end
   2.547 @@ -953,14 +945,14 @@
   2.548  (* Adjust a diagonalization to collect rationals at the start.               *)
   2.549    (* FIXME : Potentially polymorphic keys, but here only: integers!! *)
   2.550  local
   2.551 - fun upd0 x y a = if y =/ rat_0 then a else Intfunc.update(x,y) a;
   2.552 + fun upd0 x y a = if y =/ rat_0 then a else FuncUtil.Intfunc.update(x,y) a;
   2.553   fun mapa f (d,v) = 
   2.554 -  (d, Intfunc.fold (fn (i,c) => fn a => upd0 i (f c) a) v Intfunc.undefined)
   2.555 +  (d, FuncUtil.Intfunc.fold (fn (i,c) => fn a => upd0 i (f c) a) v FuncUtil.Intfunc.undefined)
   2.556   fun adj (c,l) =
   2.557   let val a = 
   2.558 -  Intfunc.fold (fn (i,c) => fn a => lcm_rat a (denominator_rat c)) 
   2.559 +  FuncUtil.Intfunc.fold (fn (i,c) => fn a => lcm_rat a (denominator_rat c)) 
   2.560      (snd l) rat_1 //
   2.561 -  Intfunc.fold (fn (i,c) => fn a => gcd_rat a (numerator_rat c)) 
   2.562 +  FuncUtil.Intfunc.fold (fn (i,c) => fn a => gcd_rat a (numerator_rat c)) 
   2.563      (snd l) rat_0
   2.564    in ((c // (a */ a)),mapa (fn x => a */ x) l)
   2.565    end
   2.566 @@ -977,11 +969,11 @@
   2.567  
   2.568  fun enumerate_monomials d vars = 
   2.569   if d < 0 then []
   2.570 - else if d = 0 then [Ctermfunc.undefined]
   2.571 + else if d = 0 then [FuncUtil.Ctermfunc.undefined]
   2.572   else if null vars then [monomial_1] else
   2.573   let val alts =
   2.574    map (fn k => let val oths = enumerate_monomials (d - k) (tl vars) 
   2.575 -               in map (fn ks => if k = 0 then ks else Ctermfunc.update (hd vars, k) ks) oths end) (0 upto d) 
   2.576 +               in map (fn ks => if k = 0 then ks else FuncUtil.Ctermfunc.update (hd vars, k) ks) oths end) (0 upto d) 
   2.577   in foldr1 op @ alts
   2.578   end;
   2.579  
   2.580 @@ -989,27 +981,23 @@
   2.581  (* We ignore any constant input polynomials.                                 *)
   2.582  (* Give the output polynomial and a record of how it was derived.            *)
   2.583  
   2.584 -local
   2.585 - open RealArith
   2.586 -in
   2.587  fun enumerate_products d pols =
   2.588 -if d = 0 then [(poly_const rat_1,Rational_lt rat_1)] 
   2.589 +if d = 0 then [(poly_const rat_1,RealArith.Rational_lt rat_1)] 
   2.590  else if d < 0 then [] else
   2.591  case pols of 
   2.592 -   [] => [(poly_const rat_1,Rational_lt rat_1)]
   2.593 +   [] => [(poly_const rat_1,RealArith.Rational_lt rat_1)]
   2.594   | (p,b)::ps => 
   2.595      let val e = multidegree p 
   2.596      in if e = 0 then enumerate_products d ps else
   2.597         enumerate_products d ps @
   2.598 -       map (fn (q,c) => (poly_mul p q,Product(b,c)))
   2.599 +       map (fn (q,c) => (poly_mul p q,RealArith.Product(b,c)))
   2.600           (enumerate_products (d - e) ps)
   2.601      end
   2.602 -end;
   2.603  
   2.604  (* Convert regular polynomial. Note that we treat (0,0,0) as -1.             *)
   2.605  
   2.606  fun epoly_of_poly p =
   2.607 -  Monomialfunc.fold (fn (m,c) => fn a => Monomialfunc.update (m, Inttriplefunc.onefunc ((0,0,0), Rat.neg c)) a) p Monomialfunc.undefined;
   2.608 +  FuncUtil.Monomialfunc.fold (fn (m,c) => fn a => FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0,0,0), Rat.neg c)) a) p FuncUtil.Monomialfunc.undefined;
   2.609  
   2.610  (* String for block diagonal matrix numbered k.                              *)
   2.611  
   2.612 @@ -1020,7 +1008,7 @@
   2.613      Inttriplefunc.fold 
   2.614        (fn ((b,i,j),c) => fn a => if i > j then a else ((b,i,j),c)::a) 
   2.615        m [] 
   2.616 -  val entss = sort (increasing fst triple_int_ord) ents 
   2.617 +  val entss = sort (FuncUtil.increasing fst triple_int_ord) ents 
   2.618   in fold_rev (fn ((b,i,j),c) => fn a =>
   2.619       pfx ^ string_of_int b ^ " " ^ string_of_int i ^ " " ^ string_of_int j ^
   2.620       " " ^ decimalize 20 c ^ "\n" ^ a) entss ""
   2.621 @@ -1060,8 +1048,8 @@
   2.622  fun blocks blocksizes bm =
   2.623   map (fn (bs,b0) =>
   2.624        let val m = Inttriplefunc.fold
   2.625 -          (fn ((b,i,j),c) => fn a => if b = b0 then Intpairfunc.update ((i,j),c) a else a) bm Intpairfunc.undefined
   2.626 -          val d = Intpairfunc.fold (fn ((i,j),c) => fn a => max a (max i j)) m 0 
   2.627 +          (fn ((b,i,j),c) => fn a => if b = b0 then FuncUtil.Intpairfunc.update ((i,j),c) a else a) bm FuncUtil.Intpairfunc.undefined
   2.628 +          val d = FuncUtil.Intpairfunc.fold (fn ((i,j),c) => fn a => max a (max i j)) m 0 
   2.629        in (((bs,bs),m):matrix) end)
   2.630   (blocksizes ~~ (1 upto length blocksizes));;
   2.631  
   2.632 @@ -1076,15 +1064,12 @@
   2.633  (* Positiv- and Nullstellensatz. Flag "linf" forces a linear representation. *)
   2.634  
   2.635   
   2.636 -local
   2.637 - open RealArith
   2.638 -in
   2.639  fun real_positivnullstellensatz_general prover linf d eqs leqs pol =
   2.640  let 
   2.641   val vars = fold_rev (curry (gen_union (op aconvc)) o poly_variables) 
   2.642                (pol::eqs @ map fst leqs) []
   2.643   val monoid = if linf then 
   2.644 -      (poly_const rat_1,Rational_lt rat_1)::
   2.645 +      (poly_const rat_1,RealArith.Rational_lt rat_1)::
   2.646        (filter (fn (p,c) => multidegree p <= d) leqs)
   2.647      else enumerate_products d leqs
   2.648   val nblocks = length monoid
   2.649 @@ -1094,7 +1079,7 @@
   2.650     val mons = enumerate_monomials e vars
   2.651     val nons = mons ~~ (1 upto length mons) 
   2.652    in (mons,
   2.653 -      fold_rev (fn (m,n) => Monomialfunc.update(m,Inttriplefunc.onefunc((~k,~n,n),rat_1))) nons Monomialfunc.undefined)
   2.654 +      fold_rev (fn (m,n) => FuncUtil.Monomialfunc.update(m,Inttriplefunc.onefunc((~k,~n,n),rat_1))) nons FuncUtil.Monomialfunc.undefined)
   2.655    end
   2.656  
   2.657   fun mk_sqmultiplier k (p,c) =
   2.658 @@ -1108,11 +1093,11 @@
   2.659          let val m = monomial_mul m1 m2 
   2.660          in if n1 > n2 then a else
   2.661            let val c = if n1 = n2 then rat_1 else rat_2
   2.662 -              val e = Monomialfunc.tryapplyd a m Inttriplefunc.undefined 
   2.663 -          in Monomialfunc.update(m, tri_equation_add (Inttriplefunc.onefunc((k,n1,n2), c)) e) a
   2.664 +              val e = FuncUtil.Monomialfunc.tryapplyd a m Inttriplefunc.undefined 
   2.665 +          in FuncUtil.Monomialfunc.update(m, tri_equation_add (Inttriplefunc.onefunc((k,n1,n2), c)) e) a
   2.666            end
   2.667          end)  nons)
   2.668 -       nons Monomialfunc.undefined)
   2.669 +       nons FuncUtil.Monomialfunc.undefined)
   2.670    end
   2.671  
   2.672    val (sqmonlist,sqs) = split_list (map2 mk_sqmultiplier (1 upto length monoid) monoid)
   2.673 @@ -1122,7 +1107,7 @@
   2.674      fold_rev2 (fn p => fn q => fn a => tri_epoly_pmul p q a) eqs ids
   2.675              (fold_rev2 (fn (p,c) => fn s => fn a => tri_epoly_pmul p s a) monoid sqs
   2.676                       (epoly_of_poly(poly_neg pol)))
   2.677 -  val eqns = Monomialfunc.fold (fn (m,e) => fn a => e::a) bigsum []
   2.678 +  val eqns = FuncUtil.Monomialfunc.fold (fn (m,e) => fn a => e::a) bigsum []
   2.679    val (pvs,assig) = tri_eliminate_all_equations (0,0,0) eqns
   2.680    val qvars = (0,0,0)::pvs
   2.681    val allassig = fold_rev (fn v => Inttriplefunc.update(v,(Inttriplefunc.onefunc(v,rat_1)))) pvs assig
   2.682 @@ -1140,12 +1125,12 @@
   2.683  
   2.684    val mats = map mk_matrix qvars
   2.685    val obj = (length pvs,
   2.686 -            itern 1 pvs (fn v => fn i => Intfunc.updatep iszero (i,Inttriplefunc.tryapplyd diagents v rat_0))
   2.687 -                        Intfunc.undefined)
   2.688 +            itern 1 pvs (fn v => fn i => FuncUtil.Intfunc.updatep iszero (i,Inttriplefunc.tryapplyd diagents v rat_0))
   2.689 +                        FuncUtil.Intfunc.undefined)
   2.690    val raw_vec = if null pvs then vector_0 0
   2.691                  else tri_scale_then (run_blockproblem prover nblocks blocksizes) obj mats
   2.692 -  fun int_element (d,v) i = Intfunc.tryapplyd v i rat_0
   2.693 -  fun cterm_element (d,v) i = Ctermfunc.tryapplyd v i rat_0
   2.694 +  fun int_element (d,v) i = FuncUtil.Intfunc.tryapplyd v i rat_0
   2.695 +  fun cterm_element (d,v) i = FuncUtil.Ctermfunc.tryapplyd v i rat_0
   2.696  
   2.697    fun find_rounding d =
   2.698     let 
   2.699 @@ -1169,12 +1154,12 @@
   2.700    val finalassigs =
   2.701      Inttriplefunc.fold (fn (v,e) => fn a => Inttriplefunc.update(v, tri_equation_eval newassigs e) a) allassig newassigs
   2.702    fun poly_of_epoly p =
   2.703 -    Monomialfunc.fold (fn (v,e) => fn a => Monomialfunc.updatep iszero (v,tri_equation_eval finalassigs e) a)
   2.704 -          p Monomialfunc.undefined
   2.705 +    FuncUtil.Monomialfunc.fold (fn (v,e) => fn a => FuncUtil.Monomialfunc.updatep iszero (v,tri_equation_eval finalassigs e) a)
   2.706 +          p FuncUtil.Monomialfunc.undefined
   2.707    fun  mk_sos mons =
   2.708     let fun mk_sq (c,m) =
   2.709 -    (c,fold_rev (fn k=> fn a => Monomialfunc.updatep iszero (nth mons (k - 1), int_element m k) a)
   2.710 -                 (1 upto length mons) Monomialfunc.undefined)
   2.711 +    (c,fold_rev (fn k=> fn a => FuncUtil.Monomialfunc.updatep iszero (nth mons (k - 1), int_element m k) a)
   2.712 +                 (1 upto length mons) FuncUtil.Monomialfunc.undefined)
   2.713     in map mk_sq
   2.714     end
   2.715    val sqs = map2 mk_sos sqmonlist ratdias
   2.716 @@ -1186,13 +1171,11 @@
   2.717             (fold_rev2 (fn p => fn q => poly_add (poly_mul p q)) cfs eqs
   2.718                      (poly_neg pol))
   2.719  
   2.720 -in if not(Monomialfunc.is_undefined sanity) then raise Sanity else
   2.721 +in if not(FuncUtil.Monomialfunc.is_undefined sanity) then raise Sanity else
   2.722    (cfs,map (fn (a,b) => (snd a,b)) msq)
   2.723   end
   2.724  
   2.725  
   2.726 -end;
   2.727 -
   2.728  (* Iterative deepening.                                                      *)
   2.729  
   2.730  fun deepen f n = 
   2.731 @@ -1201,21 +1184,15 @@
   2.732  
   2.733  (* Map back polynomials and their composites to a positivstellensatz.        *)
   2.734  
   2.735 -local
   2.736 - open Thm Numeral RealArith
   2.737 -in
   2.738 -
   2.739 -fun cterm_of_sqterm (c,p) = Product(Rational_lt c,Square p);
   2.740 +fun cterm_of_sqterm (c,p) = RealArith.Product(RealArith.Rational_lt c,RealArith.Square p);
   2.741  
   2.742  fun cterm_of_sos (pr,sqs) = if null sqs then pr
   2.743 -  else Product(pr,foldr1 (fn (a, b) => Sum(a,b)) (map cterm_of_sqterm sqs));
   2.744 -
   2.745 -end
   2.746 +  else RealArith.Product(pr,foldr1 (fn (a, b) => RealArith.Sum(a,b)) (map cterm_of_sqterm sqs));
   2.747  
   2.748  (* Interface to HOL.                                                         *)
   2.749  local
   2.750 -  open Thm Conv RealArith
   2.751 -  val concl = dest_arg o cprop_of
   2.752 +  open Conv
   2.753 +  val concl = Thm.dest_arg o cprop_of
   2.754    fun simple_cterm_ord t u = TermOrd.fast_term_ord (term_of t, term_of u) = LESS
   2.755  in
   2.756    (* FIXME: Replace tryfind by get_first !! *)
   2.757 @@ -1228,37 +1205,37 @@
   2.758         real_poly_pow_conv,real_poly_sub_conv,real_poly_conv) = (add,mul,neg,pow,sub,main)
   2.759    fun mainf cert_choice translator (eqs,les,lts) = 
   2.760    let 
   2.761 -   val eq0 = map (poly_of_term o dest_arg1 o concl) eqs
   2.762 -   val le0 = map (poly_of_term o dest_arg o concl) les
   2.763 -   val lt0 = map (poly_of_term o dest_arg o concl) lts
   2.764 -   val eqp0 = map (fn (t,i) => (t,Axiom_eq i)) (eq0 ~~ (0 upto (length eq0 - 1)))
   2.765 -   val lep0 = map (fn (t,i) => (t,Axiom_le i)) (le0 ~~ (0 upto (length le0 - 1)))
   2.766 -   val ltp0 = map (fn (t,i) => (t,Axiom_lt i)) (lt0 ~~ (0 upto (length lt0 - 1)))
   2.767 +   val eq0 = map (poly_of_term o Thm.dest_arg1 o concl) eqs
   2.768 +   val le0 = map (poly_of_term o Thm.dest_arg o concl) les
   2.769 +   val lt0 = map (poly_of_term o Thm.dest_arg o concl) lts
   2.770 +   val eqp0 = map (fn (t,i) => (t,RealArith.Axiom_eq i)) (eq0 ~~ (0 upto (length eq0 - 1)))
   2.771 +   val lep0 = map (fn (t,i) => (t,RealArith.Axiom_le i)) (le0 ~~ (0 upto (length le0 - 1)))
   2.772 +   val ltp0 = map (fn (t,i) => (t,RealArith.Axiom_lt i)) (lt0 ~~ (0 upto (length lt0 - 1)))
   2.773     val (keq,eq) = List.partition (fn (p,_) => multidegree p = 0) eqp0
   2.774     val (klep,lep) = List.partition (fn (p,_) => multidegree p = 0) lep0
   2.775     val (kltp,ltp) = List.partition (fn (p,_) => multidegree p = 0) ltp0
   2.776     fun trivial_axiom (p,ax) =
   2.777      case ax of
   2.778 -       Axiom_eq n => if eval Ctermfunc.undefined p <>/ Rat.zero then nth eqs n 
   2.779 +       RealArith.Axiom_eq n => if eval FuncUtil.Ctermfunc.undefined p <>/ Rat.zero then nth eqs n 
   2.780                       else raise Failure "trivial_axiom: Not a trivial axiom"
   2.781 -     | Axiom_le n => if eval Ctermfunc.undefined p </ Rat.zero then nth les n 
   2.782 +     | RealArith.Axiom_le n => if eval FuncUtil.Ctermfunc.undefined p </ Rat.zero then nth les n 
   2.783                       else raise Failure "trivial_axiom: Not a trivial axiom"
   2.784 -     | Axiom_lt n => if eval Ctermfunc.undefined p <=/ Rat.zero then nth lts n 
   2.785 +     | RealArith.Axiom_lt n => if eval FuncUtil.Ctermfunc.undefined p <=/ Rat.zero then nth lts n 
   2.786                       else raise Failure "trivial_axiom: Not a trivial axiom"
   2.787       | _ => error "trivial_axiom: Not a trivial axiom"
   2.788     in 
   2.789    (let val th = tryfind trivial_axiom (keq @ klep @ kltp)
   2.790     in
   2.791 -    (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv field_comp_conv) th, Trivial)
   2.792 +    (fconv_rule (arg_conv (arg1_conv real_poly_conv) then_conv field_comp_conv) th, RealArith.Trivial)
   2.793     end)
   2.794     handle Failure _ => 
   2.795       (let val proof =
   2.796         (case proof_method of Certificate certs =>
   2.797           (* choose certificate *)
   2.798           let
   2.799 -           fun chose_cert [] (Cert c) = c
   2.800 -             | chose_cert (Left::s) (Branch (l, _)) = chose_cert s l
   2.801 -             | chose_cert (Right::s) (Branch (_, r)) = chose_cert s r
   2.802 +           fun chose_cert [] (RealArith.Cert c) = c
   2.803 +             | chose_cert (RealArith.Left::s) (RealArith.Branch (l, _)) = chose_cert s l
   2.804 +             | chose_cert (RealArith.Right::s) (RealArith.Branch (_, r)) = chose_cert s r
   2.805               | chose_cert _ _ = error "certificate tree in invalid form"
   2.806           in
   2.807             chose_cert cert_choice certs
   2.808 @@ -1278,17 +1255,17 @@
   2.809             end
   2.810           val (d,i,(cert_ideal,cert_cone)) = deepen tryall 0
   2.811           val proofs_ideal =
   2.812 -           map2 (fn q => fn (p,ax) => Eqmul(q,ax)) cert_ideal eq
   2.813 +           map2 (fn q => fn (p,ax) => RealArith.Eqmul(q,ax)) cert_ideal eq
   2.814           val proofs_cone = map cterm_of_sos cert_cone
   2.815 -         val proof_ne = if null ltp then Rational_lt Rat.one else
   2.816 -           let val p = foldr1 (fn (s, t) => Product(s,t)) (map snd ltp) 
   2.817 -           in  funpow i (fn q => Product(p,q)) (Rational_lt Rat.one)
   2.818 +         val proof_ne = if null ltp then RealArith.Rational_lt Rat.one else
   2.819 +           let val p = foldr1 (fn (s, t) => RealArith.Product(s,t)) (map snd ltp) 
   2.820 +           in  funpow i (fn q => RealArith.Product(p,q)) (RealArith.Rational_lt Rat.one)
   2.821             end
   2.822           in 
   2.823 -           foldr1 (fn (s, t) => Sum(s,t)) (proof_ne :: proofs_ideal @ proofs_cone) 
   2.824 +           foldr1 (fn (s, t) => RealArith.Sum(s,t)) (proof_ne :: proofs_ideal @ proofs_cone) 
   2.825           end)
   2.826       in
   2.827 -        (translator (eqs,les,lts) proof, Cert proof)
   2.828 +        (translator (eqs,les,lts) proof, RealArith.Cert proof)
   2.829       end)
   2.830     end
   2.831   in mainf end
   2.832 @@ -1305,9 +1282,9 @@
   2.833  (* A wrapper that tries to substitute away variables first.                  *)
   2.834  
   2.835  local
   2.836 - open Thm Conv RealArith
   2.837 + open Conv
   2.838    fun simple_cterm_ord t u = TermOrd.fast_term_ord (term_of t, term_of u) = LESS
   2.839 - val concl = dest_arg o cprop_of
   2.840 + val concl = Thm.dest_arg o cprop_of
   2.841   val shuffle1 = 
   2.842     fconv_rule (rewr_conv @{lemma "(a + x == y) == (x == y - (a::real))" by (atomize (full)) (simp add: ring_simps) })
   2.843   val shuffle2 =
   2.844 @@ -1316,19 +1293,19 @@
   2.845      Free(_,@{typ real}) => if not (member (op aconvc) fvs tm) then (Rat.one,tm) 
   2.846                             else raise Failure "substitutable_monomial"
   2.847    | @{term "op * :: real => _"}$c$(t as Free _ ) => 
   2.848 -     if is_ratconst (dest_arg1 tm) andalso not (member (op aconvc) fvs (dest_arg tm))
   2.849 -         then (dest_ratconst (dest_arg1 tm),dest_arg tm) else raise Failure "substitutable_monomial"
   2.850 +     if RealArith.is_ratconst (Thm.dest_arg1 tm) andalso not (member (op aconvc) fvs (Thm.dest_arg tm))
   2.851 +         then (RealArith.dest_ratconst (Thm.dest_arg1 tm),Thm.dest_arg tm) else raise Failure "substitutable_monomial"
   2.852    | @{term "op + :: real => _"}$s$t => 
   2.853 -       (substitutable_monomial (add_cterm_frees (dest_arg tm) fvs) (dest_arg1 tm)
   2.854 -        handle Failure _ => substitutable_monomial (add_cterm_frees (dest_arg1 tm) fvs) (dest_arg tm))
   2.855 +       (substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg tm) fvs) (Thm.dest_arg1 tm)
   2.856 +        handle Failure _ => substitutable_monomial (Thm.add_cterm_frees (Thm.dest_arg1 tm) fvs) (Thm.dest_arg tm))
   2.857    | _ => raise Failure "substitutable_monomial"
   2.858  
   2.859    fun isolate_variable v th = 
   2.860 -   let val w = dest_arg1 (cprop_of th)
   2.861 +   let val w = Thm.dest_arg1 (cprop_of th)
   2.862     in if v aconvc w then th
   2.863        else case term_of w of
   2.864             @{term "op + :: real => _"}$s$t => 
   2.865 -              if dest_arg1 w aconvc v then shuffle2 th 
   2.866 +              if Thm.dest_arg1 w aconvc v then shuffle2 th 
   2.867                else isolate_variable v (shuffle1 th)
   2.868            | _ => error "isolate variable : This should not happen?"
   2.869     end 
   2.870 @@ -1345,8 +1322,8 @@
   2.871  
   2.872    fun make_substitution th =
   2.873     let 
   2.874 -    val (c,v) = substitutable_monomial [] (dest_arg1(concl th))
   2.875 -    val th1 = Drule.arg_cong_rule (capply @{cterm "op * :: real => _"} (cterm_of_rat (Rat.inv c))) (mk_meta_eq th)
   2.876 +    val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th))
   2.877 +    val th1 = Drule.arg_cong_rule (Thm.capply @{cterm "op * :: real => _"} (RealArith.cterm_of_rat (Rat.inv c))) (mk_meta_eq th)
   2.878      val th2 = fconv_rule (binop_conv real_poly_mul_conv) th1
   2.879     in fconv_rule (arg_conv real_poly_conv) (isolate_variable v th2)
   2.880     end
   2.881 @@ -1378,7 +1355,7 @@
   2.882  (* Overall function. *)
   2.883  
   2.884  fun real_sos prover ctxt =
   2.885 -  gen_prover_real_arith ctxt (real_nonlinear_subst_prover prover ctxt)
   2.886 +  RealArith.gen_prover_real_arith ctxt (real_nonlinear_subst_prover prover ctxt)
   2.887  end;
   2.888  
   2.889  (* A tactic *)
     3.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Oct 01 18:59:26 2009 +0200
     3.2 +++ b/src/HOL/Library/positivstellensatz.ML	Tue Sep 22 14:17:54 2009 +0200
     3.3 @@ -165,7 +165,7 @@
     3.4  structure RealArith : REAL_ARITH =
     3.5  struct
     3.6  
     3.7 - open Conv Thm FuncUtil;;
     3.8 + open Conv
     3.9  (* ------------------------------------------------------------------------- *)
    3.10  (* Data structure for Positivstellensatz refutations.                        *)
    3.11  (* ------------------------------------------------------------------------- *)
    3.12 @@ -353,36 +353,31 @@
    3.13  
    3.14  (* Map back polynomials to HOL.                         *)
    3.15  
    3.16 -local
    3.17 - open Thm Numeral
    3.18 -in
    3.19 -
    3.20 -fun cterm_of_varpow x k = if k = 1 then x else capply (capply @{cterm "op ^ :: real => _"} x) 
    3.21 -  (mk_cnumber @{ctyp nat} k)
    3.22 +fun cterm_of_varpow x k = if k = 1 then x else Thm.capply (Thm.capply @{cterm "op ^ :: real => _"} x) 
    3.23 +  (Numeral.mk_cnumber @{ctyp nat} k)
    3.24  
    3.25  fun cterm_of_monomial m = 
    3.26 - if Ctermfunc.is_undefined m then @{cterm "1::real"} 
    3.27 + if FuncUtil.Ctermfunc.is_undefined m then @{cterm "1::real"} 
    3.28   else 
    3.29    let 
    3.30 -   val m' = dest_monomial m
    3.31 +   val m' = FuncUtil.dest_monomial m
    3.32     val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' [] 
    3.33 -  in foldr1 (fn (s, t) => capply (capply @{cterm "op * :: real => _"} s) t) vps
    3.34 +  in foldr1 (fn (s, t) => Thm.capply (Thm.capply @{cterm "op * :: real => _"} s) t) vps
    3.35    end
    3.36  
    3.37 -fun cterm_of_cmonomial (m,c) = if Ctermfunc.is_undefined m then cterm_of_rat c
    3.38 +fun cterm_of_cmonomial (m,c) = if FuncUtil.Ctermfunc.is_undefined m then cterm_of_rat c
    3.39      else if c = Rat.one then cterm_of_monomial m
    3.40 -    else capply (capply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
    3.41 +    else Thm.capply (Thm.capply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
    3.42  
    3.43  fun cterm_of_poly p = 
    3.44 - if Monomialfunc.is_undefined p then @{cterm "0::real"} 
    3.45 + if FuncUtil.Monomialfunc.is_undefined p then @{cterm "0::real"} 
    3.46   else
    3.47    let 
    3.48     val cms = map cterm_of_cmonomial
    3.49 -     (sort (prod_ord monomial_order (K EQUAL)) (Monomialfunc.graph p))
    3.50 -  in foldr1 (fn (t1, t2) => capply(capply @{cterm "op + :: real => _"} t1) t2) cms
    3.51 +     (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.graph p))
    3.52 +  in foldr1 (fn (t1, t2) => Thm.capply(Thm.capply @{cterm "op + :: real => _"} t1) t2) cms
    3.53    end;
    3.54  
    3.55 -end;
    3.56      (* A general real arithmetic prover *)
    3.57  
    3.58  fun gen_gen_real_arith ctxt (mk_numeric,
    3.59 @@ -390,7 +385,6 @@
    3.60         poly_conv,poly_neg_conv,poly_add_conv,poly_mul_conv,
    3.61         absconv1,absconv2,prover) = 
    3.62  let
    3.63 - open Conv Thm;
    3.64   val _ = my_context := ctxt 
    3.65   val _ = (my_mk_numeric := mk_numeric ; my_numeric_eq_conv := numeric_eq_conv ; 
    3.66            my_numeric_ge_conv := numeric_ge_conv; my_numeric_gt_conv := numeric_gt_conv ;
    3.67 @@ -414,7 +408,7 @@
    3.68  
    3.69   fun real_ineq_conv th ct =
    3.70    let
    3.71 -   val th' = (instantiate (match (lhs_of th, ct)) th 
    3.72 +   val th' = (Thm.instantiate (Thm.match (Thm.lhs_of th, ct)) th 
    3.73        handle MATCH => raise CTERM ("real_ineq_conv", [ct]))
    3.74    in transitive th' (oprconv poly_conv (Thm.rhs_of th'))
    3.75    end 
    3.76 @@ -442,14 +436,14 @@
    3.77          Axiom_eq n => nth eqs n
    3.78        | Axiom_le n => nth les n
    3.79        | Axiom_lt n => nth lts n
    3.80 -      | Rational_eq x => eqT_elim(numeric_eq_conv(capply @{cterm Trueprop} 
    3.81 -                          (capply (capply @{cterm "op =::real => _"} (mk_numeric x)) 
    3.82 +      | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.capply @{cterm Trueprop} 
    3.83 +                          (Thm.capply (Thm.capply @{cterm "op =::real => _"} (mk_numeric x)) 
    3.84                                 @{cterm "0::real"})))
    3.85 -      | Rational_le x => eqT_elim(numeric_ge_conv(capply @{cterm Trueprop} 
    3.86 -                          (capply (capply @{cterm "op <=::real => _"} 
    3.87 +      | Rational_le x => eqT_elim(numeric_ge_conv(Thm.capply @{cterm Trueprop} 
    3.88 +                          (Thm.capply (Thm.capply @{cterm "op <=::real => _"} 
    3.89                                       @{cterm "0::real"}) (mk_numeric x))))
    3.90 -      | Rational_lt x => eqT_elim(numeric_gt_conv(capply @{cterm Trueprop} 
    3.91 -                      (capply (capply @{cterm "op <::real => _"} @{cterm "0::real"})
    3.92 +      | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.capply @{cterm Trueprop} 
    3.93 +                      (Thm.capply (Thm.capply @{cterm "op <::real => _"} @{cterm "0::real"})
    3.94                          (mk_numeric x))))
    3.95        | Square pt => square_rule (cterm_of_poly pt)
    3.96        | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
    3.97 @@ -463,8 +457,8 @@
    3.98        nnf_conv then_conv skolemize_conv then_conv prenex_conv then_conv
    3.99        weak_dnf_conv
   3.100  
   3.101 -  val concl = dest_arg o cprop_of
   3.102 -  fun is_binop opr ct = (dest_fun2 ct aconvc opr handle CTERM _ => false)
   3.103 +  val concl = Thm.dest_arg o cprop_of
   3.104 +  fun is_binop opr ct = (Thm.dest_fun2 ct aconvc opr handle CTERM _ => false)
   3.105    val is_req = is_binop @{cterm "op =:: real => _"}
   3.106    val is_ge = is_binop @{cterm "op <=:: real => _"}
   3.107    val is_gt = is_binop @{cterm "op <:: real => _"}
   3.108 @@ -472,10 +466,13 @@
   3.109    val is_disj = is_binop @{cterm "op |"}
   3.110    fun conj_pair th = (th RS @{thm conjunct1}, th RS @{thm conjunct2})
   3.111    fun disj_cases th th1 th2 = 
   3.112 -   let val (p,q) = dest_binop (concl th)
   3.113 +   let val (p,q) = Thm.dest_binop (concl th)
   3.114         val c = concl th1
   3.115         val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
   3.116 -   in implies_elim (implies_elim (implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th) (implies_intr (capply @{cterm Trueprop} p) th1)) (implies_intr (capply @{cterm Trueprop} q) th2)
   3.117 +   in implies_elim (implies_elim
   3.118 +          (implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
   3.119 +          (implies_intr (Thm.capply @{cterm Trueprop} p) th1))
   3.120 +        (implies_intr (Thm.capply @{cterm Trueprop} q) th2)
   3.121     end
   3.122   fun overall cert_choice dun ths = case ths of
   3.123    [] =>
   3.124 @@ -494,37 +491,37 @@
   3.125        overall cert_choice dun (th1::th2::oths) end
   3.126      else if is_disj ct then
   3.127        let 
   3.128 -       val (th1, cert1) = overall (Left::cert_choice) dun (assume (capply @{cterm Trueprop} (dest_arg1 ct))::oths)
   3.129 -       val (th2, cert2) = overall (Right::cert_choice) dun (assume (capply @{cterm Trueprop} (dest_arg ct))::oths)
   3.130 +       val (th1, cert1) = overall (Left::cert_choice) dun (assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
   3.131 +       val (th2, cert2) = overall (Right::cert_choice) dun (assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
   3.132        in (disj_cases th th1 th2, Branch (cert1, cert2)) end
   3.133     else overall cert_choice (th::dun) oths
   3.134    end
   3.135 -  fun dest_binary b ct = if is_binop b ct then dest_binop ct 
   3.136 +  fun dest_binary b ct = if is_binop b ct then Thm.dest_binop ct 
   3.137                           else raise CTERM ("dest_binary",[b,ct])
   3.138    val dest_eq = dest_binary @{cterm "op = :: real => _"}
   3.139    val neq_th = nth pth 5
   3.140    fun real_not_eq_conv ct = 
   3.141     let 
   3.142 -    val (l,r) = dest_eq (dest_arg ct)
   3.143 -    val th = instantiate ([],[(@{cpat "?x::real"},l),(@{cpat "?y::real"},r)]) neq_th
   3.144 -    val th_p = poly_conv(dest_arg(dest_arg1(rhs_of th)))
   3.145 +    val (l,r) = dest_eq (Thm.dest_arg ct)
   3.146 +    val th = Thm.instantiate ([],[(@{cpat "?x::real"},l),(@{cpat "?y::real"},r)]) neq_th
   3.147 +    val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
   3.148      val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
   3.149      val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
   3.150      val th' = Drule.binop_cong_rule @{cterm "op |"} 
   3.151 -     (Drule.arg_cong_rule (capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
   3.152 -     (Drule.arg_cong_rule (capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
   3.153 +     (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
   3.154 +     (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
   3.155      in transitive th th' 
   3.156    end
   3.157   fun equal_implies_1_rule PQ = 
   3.158    let 
   3.159 -   val P = lhs_of PQ
   3.160 +   val P = Thm.lhs_of PQ
   3.161    in implies_intr P (equal_elim PQ (assume P))
   3.162    end
   3.163   (* FIXME!!! Copied from groebner.ml *)
   3.164   val strip_exists =
   3.165    let fun h (acc, t) =
   3.166     case (term_of t) of
   3.167 -    Const("Ex",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
   3.168 +    Const("Ex",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   3.169    | _ => (acc,t)
   3.170    in fn t => h ([],t)
   3.171    end
   3.172 @@ -559,7 +556,7 @@
   3.173   val strip_forall =
   3.174    let fun h (acc, t) =
   3.175     case (term_of t) of
   3.176 -    Const("All",_)$Abs(x,T,p) => h (dest_abs NONE (dest_arg t) |>> (fn v => v::acc))
   3.177 +    Const("All",_)$Abs(x,T,p) => h (Thm.dest_abs NONE (Thm.dest_arg t) |>> (fn v => v::acc))
   3.178    | _ => (acc,t)
   3.179    in fn t => h ([],t)
   3.180    end
   3.181 @@ -576,16 +573,16 @@
   3.182    fun absremover ct = (literals_conv [@{term "op &"}, @{term "op |"}] [] 
   3.183                    (try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv 
   3.184          try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
   3.185 -  val nct = capply @{cterm Trueprop} (capply @{cterm "Not"} ct)
   3.186 +  val nct = Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} ct)
   3.187    val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct
   3.188 -  val tm0 = dest_arg (rhs_of th0)
   3.189 +  val tm0 = Thm.dest_arg (Thm.rhs_of th0)
   3.190    val (th, certificates) = if tm0 aconvc @{cterm False} then (equal_implies_1_rule th0, Trivial) else
   3.191     let 
   3.192      val (evs,bod) = strip_exists tm0
   3.193      val (avs,ibod) = strip_forall bod
   3.194      val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
   3.195 -    val (th2, certs) = overall [] [] [specl avs (assume (rhs_of th1))]
   3.196 -    val th3 = fold simple_choose evs (prove_hyp (equal_elim th1 (assume (capply @{cterm Trueprop} bod))) th2)
   3.197 +    val (th2, certs) = overall [] [] [specl avs (assume (Thm.rhs_of th1))]
   3.198 +    val th3 = fold simple_choose evs (prove_hyp (equal_elim th1 (assume (Thm.capply @{cterm Trueprop} bod))) th2)
   3.199     in (Drule.implies_intr_hyps (prove_hyp (equal_elim th0 (assume nct)) th3), certs)
   3.200     end
   3.201    in (implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
   3.202 @@ -595,11 +592,11 @@
   3.203  
   3.204  (* A linear arithmetic prover *)
   3.205  local
   3.206 -  val linear_add = Ctermfunc.combine (curry op +/) (fn z => z =/ Rat.zero)
   3.207 -  fun linear_cmul c = Ctermfunc.mapf (fn x => c */ x)
   3.208 +  val linear_add = FuncUtil.Ctermfunc.combine (curry op +/) (fn z => z =/ Rat.zero)
   3.209 +  fun linear_cmul c = FuncUtil.Ctermfunc.mapf (fn x => c */ x)
   3.210    val one_tm = @{cterm "1::real"}
   3.211 -  fun contradictory p (e,_) = ((Ctermfunc.is_undefined e) andalso not(p Rat.zero)) orelse
   3.212 -     ((gen_eq_set (op aconvc) (Ctermfunc.dom e, [one_tm])) andalso not(p(Ctermfunc.apply e one_tm)))
   3.213 +  fun contradictory p (e,_) = ((FuncUtil.Ctermfunc.is_undefined e) andalso not(p Rat.zero)) orelse
   3.214 +     ((gen_eq_set (op aconvc) (FuncUtil.Ctermfunc.dom e, [one_tm])) andalso not(p(FuncUtil.Ctermfunc.apply e one_tm)))
   3.215  
   3.216    fun linear_ineqs vars (les,lts) = 
   3.217     case find_first (contradictory (fn x => x >/ Rat.zero)) lts of
   3.218 @@ -612,15 +609,15 @@
   3.219       let 
   3.220        val ineqs = les @ lts
   3.221        fun blowup v =
   3.222 -       length(filter (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) ineqs) +
   3.223 -       length(filter (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) ineqs) *
   3.224 -       length(filter (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero </ Rat.zero) ineqs)
   3.225 +       length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) ineqs) +
   3.226 +       length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) ineqs) *
   3.227 +       length(filter (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero </ Rat.zero) ineqs)
   3.228        val  v = fst(hd(sort (fn ((_,i),(_,j)) => int_ord (i,j))
   3.229                   (map (fn v => (v,blowup v)) vars)))
   3.230        fun addup (e1,p1) (e2,p2) acc =
   3.231         let 
   3.232 -        val c1 = Ctermfunc.tryapplyd e1 v Rat.zero 
   3.233 -        val c2 = Ctermfunc.tryapplyd e2 v Rat.zero
   3.234 +        val c1 = FuncUtil.Ctermfunc.tryapplyd e1 v Rat.zero 
   3.235 +        val c2 = FuncUtil.Ctermfunc.tryapplyd e2 v Rat.zero
   3.236         in if c1 */ c2 >=/ Rat.zero then acc else
   3.237          let 
   3.238           val e1' = linear_cmul (Rat.abs c2) e1
   3.239 @@ -631,13 +628,13 @@
   3.240          end
   3.241         end
   3.242        val (les0,les1) = 
   3.243 -         List.partition (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) les
   3.244 +         List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) les
   3.245        val (lts0,lts1) = 
   3.246 -         List.partition (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) lts
   3.247 +         List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero =/ Rat.zero) lts
   3.248        val (lesp,lesn) = 
   3.249 -         List.partition (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) les1
   3.250 +         List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) les1
   3.251        val (ltsp,ltsn) = 
   3.252 -         List.partition (fn (e,_) => Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) lts1
   3.253 +         List.partition (fn (e,_) => FuncUtil.Ctermfunc.tryapplyd e v Rat.zero >/ Rat.zero) lts1
   3.254        val les' = fold_rev (fn ep1 => fold_rev (addup ep1) lesp) lesn les0
   3.255        val lts' = fold_rev (fn ep1 => fold_rev (addup ep1) (lesp@ltsp)) ltsn
   3.256                        (fold_rev (fn ep1 => fold_rev (addup ep1) (lesn@ltsn)) ltsp lts0)
   3.257 @@ -650,20 +647,20 @@
   3.258    | NONE => (case eqs of 
   3.259      [] => 
   3.260       let val vars = remove (op aconvc) one_tm 
   3.261 -           (fold_rev (curry (gen_union (op aconvc)) o Ctermfunc.dom o fst) (les@lts) []) 
   3.262 +           (fold_rev (curry (gen_union (op aconvc)) o FuncUtil.Ctermfunc.dom o fst) (les@lts) []) 
   3.263       in linear_ineqs vars (les,lts) end
   3.264     | (e,p)::es => 
   3.265 -     if Ctermfunc.is_undefined e then linear_eqs (es,les,lts) else
   3.266 +     if FuncUtil.Ctermfunc.is_undefined e then linear_eqs (es,les,lts) else
   3.267       let 
   3.268 -      val (x,c) = Ctermfunc.choose (Ctermfunc.undefine one_tm e)
   3.269 +      val (x,c) = FuncUtil.Ctermfunc.choose (FuncUtil.Ctermfunc.undefine one_tm e)
   3.270        fun xform (inp as (t,q)) =
   3.271 -       let val d = Ctermfunc.tryapplyd t x Rat.zero in
   3.272 +       let val d = FuncUtil.Ctermfunc.tryapplyd t x Rat.zero in
   3.273          if d =/ Rat.zero then inp else
   3.274          let 
   3.275           val k = (Rat.neg d) */ Rat.abs c // c
   3.276           val e' = linear_cmul k e
   3.277           val t' = linear_cmul (Rat.abs c) t
   3.278 -         val p' = Eqmul(Monomialfunc.onefunc (Ctermfunc.undefined, k),p)
   3.279 +         val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.undefined, k),p)
   3.280           val q' = Product(Rational_lt(Rat.abs c),q) 
   3.281          in (linear_add e' t',Sum(p',q')) 
   3.282          end 
   3.283 @@ -680,19 +677,19 @@
   3.284     end 
   3.285    
   3.286    fun lin_of_hol ct = 
   3.287 -   if ct aconvc @{cterm "0::real"} then Ctermfunc.undefined
   3.288 -   else if not (is_comb ct) then Ctermfunc.onefunc (ct, Rat.one)
   3.289 -   else if is_ratconst ct then Ctermfunc.onefunc (one_tm, dest_ratconst ct)
   3.290 +   if ct aconvc @{cterm "0::real"} then FuncUtil.Ctermfunc.undefined
   3.291 +   else if not (is_comb ct) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   3.292 +   else if is_ratconst ct then FuncUtil.Ctermfunc.onefunc (one_tm, dest_ratconst ct)
   3.293     else
   3.294      let val (lop,r) = Thm.dest_comb ct 
   3.295 -    in if not (is_comb lop) then Ctermfunc.onefunc (ct, Rat.one)
   3.296 +    in if not (is_comb lop) then FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   3.297         else
   3.298          let val (opr,l) = Thm.dest_comb lop 
   3.299          in if opr aconvc @{cterm "op + :: real =>_"} 
   3.300             then linear_add (lin_of_hol l) (lin_of_hol r)
   3.301             else if opr aconvc @{cterm "op * :: real =>_"} 
   3.302 -                   andalso is_ratconst l then Ctermfunc.onefunc (r, dest_ratconst l)
   3.303 -           else Ctermfunc.onefunc (ct, Rat.one)
   3.304 +                   andalso is_ratconst l then FuncUtil.Ctermfunc.onefunc (r, dest_ratconst l)
   3.305 +           else FuncUtil.Ctermfunc.onefunc (ct, Rat.one)
   3.306          end
   3.307      end
   3.308  
   3.309 @@ -700,21 +697,20 @@
   3.310     Const(@{const_name "real"}, _)$ n => 
   3.311       if can HOLogic.dest_number n then false else true
   3.312    | _ => false
   3.313 - open Thm
   3.314  in 
   3.315  fun real_linear_prover translator (eq,le,lt) = 
   3.316   let 
   3.317 -  val lhs = lin_of_hol o dest_arg1 o dest_arg o cprop_of
   3.318 -  val rhs = lin_of_hol o dest_arg o dest_arg o cprop_of
   3.319 +  val lhs = lin_of_hol o Thm.dest_arg1 o Thm.dest_arg o cprop_of
   3.320 +  val rhs = lin_of_hol o Thm.dest_arg o Thm.dest_arg o cprop_of
   3.321    val eq_pols = map lhs eq
   3.322    val le_pols = map rhs le
   3.323    val lt_pols = map rhs lt 
   3.324    val aliens =  filter is_alien
   3.325 -      (fold_rev (curry (gen_union (op aconvc)) o Ctermfunc.dom) 
   3.326 +      (fold_rev (curry (gen_union (op aconvc)) o FuncUtil.Ctermfunc.dom) 
   3.327            (eq_pols @ le_pols @ lt_pols) [])
   3.328 -  val le_pols' = le_pols @ map (fn v => Ctermfunc.onefunc (v,Rat.one)) aliens
   3.329 +  val le_pols' = le_pols @ map (fn v => FuncUtil.Ctermfunc.onefunc (v,Rat.one)) aliens
   3.330    val (_,proof) = linear_prover (eq_pols,le_pols',lt_pols)
   3.331 -  val le' = le @ map (fn a => instantiate' [] [SOME (dest_arg a)] @{thm real_of_nat_ge_zero}) aliens 
   3.332 +  val le' = le @ map (fn a => instantiate' [] [SOME (Thm.dest_arg a)] @{thm real_of_nat_ge_zero}) aliens 
   3.333   in ((translator (eq,le',lt) proof), Trivial)
   3.334   end
   3.335  end;
   3.336 @@ -737,28 +733,28 @@
   3.337     val y_tm = @{cpat "?y::real"}
   3.338     val is_max = is_binop @{cterm "max :: real => _"}
   3.339     val is_min = is_binop @{cterm "min :: real => _"} 
   3.340 -   fun is_abs t = is_comb t andalso dest_fun t aconvc abs_tm
   3.341 +   fun is_abs t = is_comb t andalso Thm.dest_fun t aconvc abs_tm
   3.342     fun eliminate_construct p c tm =
   3.343      let 
   3.344       val t = find_cterm p tm
   3.345 -     val th0 = (symmetric o beta_conversion false) (capply (cabs t tm) t)
   3.346 -     val (p,ax) = (dest_comb o rhs_of) th0
   3.347 +     val th0 = (symmetric o beta_conversion false) (Thm.capply (Thm.cabs t tm) t)
   3.348 +     val (p,ax) = (Thm.dest_comb o Thm.rhs_of) th0
   3.349      in fconv_rule(arg_conv(binop_conv (arg_conv (beta_conversion false))))
   3.350                 (transitive th0 (c p ax))
   3.351     end
   3.352  
   3.353     val elim_abs = eliminate_construct is_abs
   3.354      (fn p => fn ax => 
   3.355 -       instantiate ([], [(p_tm,p), (x_tm, dest_arg ax)]) pth_abs)
   3.356 +       Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax)]) pth_abs)
   3.357     val elim_max = eliminate_construct is_max
   3.358      (fn p => fn ax => 
   3.359 -      let val (ax,y) = dest_comb ax 
   3.360 -      in  instantiate ([], [(p_tm,p), (x_tm, dest_arg ax), (y_tm,y)]) 
   3.361 +      let val (ax,y) = Thm.dest_comb ax 
   3.362 +      in  Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)]) 
   3.363        pth_max end)
   3.364     val elim_min = eliminate_construct is_min
   3.365      (fn p => fn ax => 
   3.366 -      let val (ax,y) = dest_comb ax 
   3.367 -      in  instantiate ([], [(p_tm,p), (x_tm, dest_arg ax), (y_tm,y)]) 
   3.368 +      let val (ax,y) = Thm.dest_comb ax 
   3.369 +      in  Thm.instantiate ([], [(p_tm,p), (x_tm, Thm.dest_arg ax), (y_tm,y)]) 
   3.370        pth_min end)
   3.371     in first_conv [elim_abs, elim_max, elim_min, all_conv]
   3.372    end;