# HG changeset patch
# User wenzelm
# Date 1191356611 -7200
# Node ID d07e56a9a0c23f13a1ed1e4a548238c4789b6fba
# Parent  636b23afee76cba5fb352ba9eb5086e8514a7d11
added add_defs_new, which strips sorts for axioms (presently inactive);

diff -r 636b23afee76 -r d07e56a9a0c2 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Tue Oct 02 22:23:30 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML	Tue Oct 02 22:23:31 2007 +0200
@@ -109,7 +109,7 @@
     val (abbrs, lthy') = lthy
       |> LocalTheory.theory_result (fold_map const decls)
     val defs = map (apsnd (pair ("", []))) abbrs;
-    
+
   in
     lthy'
     |> LocalTheory.raw_theory (fold2 (const_class some_class) decls abbrs)
@@ -179,6 +179,19 @@
   Theory.add_defs_i false false [(name, prop)] #>
   (fn thy => (Drule.unvarify (Thm.get_axiom_i thy (Sign.full_name thy name)), thy));
 
+fun add_def_new (name, prop) thy =  (* FIXME inactive --- breaks codegen *)
+  let
+    val tfrees = rev (map TFree (Term.add_tfrees prop []));
+    val tfrees' = map (fn a => TFree (a, [])) (Name.invents Name.context "'a" (length tfrees));
+    val strip_sorts = tfrees ~~ tfrees';
+    val recover_sorts = map (pairself (Thm.ctyp_of thy o Logic.varifyT)) (tfrees' ~~ tfrees);
+
+    val prop' = Term.map_types (Term.map_atyps (perhaps (AList.lookup (op =) strip_sorts))) prop;
+    val thy' = Theory.add_defs_i false false [(name, prop')] thy;
+    val axm = Thm.get_axiom_i thy' (Sign.full_name thy' name);
+    val def = Thm.instantiate (recover_sorts, []) axm;
+  in (Drule.unvarify def, thy') end;
+
 in
 
 fun defs kind args lthy0 =