src/HOLCF/Tools/domain/domain_axioms.ML
changeset 30483 0c398040969c
parent 30364 577edc39b501
child 30912 4022298c1a86
--- a/src/HOLCF/Tools/domain/domain_axioms.ML	Thu Mar 12 21:37:18 2009 +0100
+++ b/src/HOLCF/Tools/domain/domain_axioms.ML	Thu Mar 12 21:42:02 2009 +0100
@@ -108,7 +108,16 @@
     [take_def, finite_def])
 end; (* let (calc_axioms) *)
 
-fun infer_props thy = map (apsnd (FixrecPackage.legacy_infer_prop thy));
+
+(* legacy type inference *)
+
+fun legacy_infer_term thy t =
+  singleton (Syntax.check_terms (ProofContext.init thy)) (Sign.intern_term thy t);
+
+fun legacy_infer_prop thy t = legacy_infer_term thy (TypeInfer.constrain propT t);
+
+fun infer_props thy = map (apsnd (legacy_infer_prop thy));
+
 
 fun add_axioms_i x = snd o PureThy.add_axioms (map (Thm.no_attributes o apfst Binding.name) x);
 fun add_axioms_infer axms thy = add_axioms_i (infer_props thy axms) thy;