legacy_infer_term/prop -- including intern_term;

--- a/src/HOLCF/domain/axioms.ML	Sun Apr 15 14:32:05 2007 +0200
+++ b/src/HOLCF/domain/axioms.ML	Sun Apr 15 14:32:07 2007 +0200
@@ -14,8 +14,6 @@
 infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<;
 infix 9 `   ; infix 9 `% ; infix 9 `%%; infixr 9 oo;
 
-fun infer_types thy' = map (Theory.inferT_axm thy');
-
 fun calc_axioms comp_dname (eqs : eq list) n (((dname,_),cons) : eq)=
 let
 
@@ -111,11 +109,13 @@
     [take_def, finite_def])
 end; (* let *)
 
+fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy));
+
 fun add_axioms_i x = snd o PureThy.add_axioms_i (map Thm.no_attributes x);
-fun add_axioms_infer axms thy = add_axioms_i (infer_types thy axms) thy;
+fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;
 
 fun add_defs_i x = snd o (PureThy.add_defs_i false) (map Thm.no_attributes x);
-fun add_defs_infer defs thy = add_defs_i (infer_types thy defs) thy;
+fun add_defs_infer defs thy = add_defs_i (infer_props thy defs) thy;
 
 in (* local *)
 

--- a/src/HOLCF/domain/library.ML	Sun Apr 15 14:32:05 2007 +0200
+++ b/src/HOLCF/domain/library.ML	Sun Apr 15 14:32:07 2007 +0200
@@ -134,6 +134,7 @@
 val pcpoN      = "Pcpo.pcpo"
 val pcpoS      = [pcpoN];
 
+
 (* ----- support for type and mixfix expressions ----- *)
 
 infixr 5 -->;
@@ -152,20 +153,9 @@
 fun mk_lam  (x,T) = Abs(x,dummyT,T);
 fun mk_all  (x,P) = HOLogic.mk_all (x,dummyT,P);
 fun mk_ex   (x,P) = mk_exists (x,dummyT,P);
-local 
-		    fun sg [s]     = %:s
-		    |   sg (s::ss) = %%:"_classes" $ %:s $ sg ss
-	 	    |   sg _       = Imposs "library:sg";
-		    fun sf [] = %%:"_emptysort"
-		    |   sf s  = %%:"_sort" $ sg s
-		    fun tf (Type (s,args)) = Library.foldl (op $) (%:s,map tf args)
-		    |   tf (TFree(s,sort)) = %%:"_ofsort" $ %:s $ sf sort
-		    |   tf _               = Imposs "library:tf";
-in
-fun mk_constrain      (typ,T) = %%:"_constrain" $ T $ tf typ;
-fun mk_constrainall (x,typ,P) = %%:"All" $ (%%:"_constrainAbs" $ mk_lam(x,P) $ tf typ);
-end;
-end;
+fun mk_constrain      (typ,T) = TypeInfer.constrain T typ;
+fun mk_constrainall (x,typ,P) = %%:"All" $ (TypeInfer.constrain (mk_lam(x,P)) (typ --> boolT));
+end
 
 fun mk_All  (x,P) = %%:"all" $ mk_lam(x,P); (* meta universal quantification *)
 

--- a/src/HOLCF/domain/theorems.ML	Sun Apr 15 14:32:05 2007 +0200
+++ b/src/HOLCF/domain/theorems.ML	Sun Apr 15 14:32:07 2007 +0200
@@ -54,19 +54,9 @@
 
 (* ----- general proof facilities ------------------------------------------- *)
 
-(* FIXME better avoid this low-level stuff *)
-fun inferT sg pre_tm =
-  let
-    val pp = Sign.pp sg;
-    val consts = Sign.consts_of sg;
-    val (t, _) =
-      Sign.infer_types pp sg consts (K NONE) (K NONE) Name.context true
-        ([pre_tm],propT);
-  in t end;
-
 fun pg'' thy defs t tacs =
   let
-    val t' = inferT thy t;
+    val t' = FixrecPackage.legacy_infer_term thy t;
     val asms = Logic.strip_imp_prems t';
     val prop = Logic.strip_imp_concl t';
     fun tac prems =

--- a/src/HOLCF/fixrec_package.ML	Sun Apr 15 14:32:05 2007 +0200
+++ b/src/HOLCF/fixrec_package.ML	Sun Apr 15 14:32:07 2007 +0200
@@ -7,6 +7,8 @@
 
 signature FIXREC_PACKAGE =
 sig
+  val legacy_infer_term: theory -> term -> term
+  val legacy_infer_prop: theory -> term -> term
   val add_fixrec: bool -> ((string * Attrib.src list) * string) list list -> theory -> theory
   val add_fixrec_i: bool -> ((string * attribute list) * term) list list -> theory -> theory
   val add_fixpat: (string * Attrib.src list) * string list -> theory -> theory
@@ -16,6 +18,15 @@
 structure FixrecPackage: FIXREC_PACKAGE =
 struct
 
+(* legacy type inference *)
+
+fun legacy_infer_types thy (t, T) =
+  #1 (singleton (ProofContext.infer_types (ProofContext.init thy)) (Sign.intern_term thy t, T));
+
+fun legacy_infer_term thy t = legacy_infer_types thy (t, dummyT);
+fun legacy_infer_prop thy t = legacy_infer_types thy (t, propT);
+
+
 val fix_eq2 = thm "fix_eq2";
 val def_fix_ind = thm "def_fix_ind";
 
@@ -50,12 +61,6 @@
 infix 1 ===; fun S === T = %%:"op =" $ S $ T;
 infix 9 `  ; fun f ` x = %%:"Cfun.Rep_CFun" $ f $ x;
 
-(* infers the type of a term *)  (* FIXME better avoid this low-level stuff *)
-(* similar to Theory.inferT_axm, but allows any type, not just propT *)
-fun infer sg t =
-  fst (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) Name.context true
-    ([t],dummyT));
-
 (* builds the expression (LAM v. rhs) *)
 fun big_lambda v rhs = %%:"Cfun.Abs_CFun"$(Term.lambda v rhs);
 
@@ -91,12 +96,12 @@
       | defs (l::ls) r = one_def l (%%:"Cprod.cfst"`r) :: defs ls (%%:"Cprod.csnd"`r);
     val (names, pre_fixdefs) = ListPair.unzip (defs lhss fixpoint);
     
-    val fixdefs = map (Theory.inferT_axm thy) pre_fixdefs;
+    val fixdefs = map (apsnd (legacy_infer_prop thy)) pre_fixdefs;
     val (fixdef_thms, thy') =
       PureThy.add_defs_i false (map Thm.no_attributes fixdefs) thy;
     val ctuple_fixdef_thm = foldr1 (fn (x,y) => cpair_equalI OF [x,y]) fixdef_thms;
     
-    val ctuple_unfold = infer thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
+    val ctuple_unfold = legacy_infer_term thy' (mk_trp (mk_ctuple lhss === mk_ctuple rhss));
     val ctuple_unfold_thm = Goal.prove_global thy' [] [] ctuple_unfold
           (fn _ => EVERY [rtac (ctuple_fixdef_thm RS fix_eq2 RS trans) 1,
                     simp_tac (simpset_of thy') 1]);
@@ -232,7 +237,7 @@
     fun unconcat [] _ = []
       | unconcat (n::ns) xs = List.take (xs,n) :: unconcat ns (List.drop (xs,n));
     val pattern_blocks = unconcat lengths (map Logic.strip_imp_concl eqn_ts');
-    val compiled_ts = map (infer thy o compile_pats) pattern_blocks;
+    val compiled_ts = map (legacy_infer_term thy o compile_pats) pattern_blocks;
     val (thy', cnames, fixdef_thms, unfold_thms) = add_fixdefs compiled_ts thy;
   in
     if strict then let (* only prove simp rules if strict = true *)