tmp hack get back to old 'constdefs';

--- a/src/HOL/Import/HOL/ROOT.ML	Thu Apr 22 11:01:34 2004 +0200
+++ b/src/HOL/Import/HOL/ROOT.ML	Thu Apr 22 11:02:22 2004 +0200
@@ -3,6 +3,29 @@
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
+(* FIXME tmp hack to get generated theories work *)
+
+local
+
+fun old_add_constdefs args thy =
+  thy
+  |> Theory.add_consts (map fst args)
+  |> IsarThy.add_defs (false, map (fn ((c, _, mx), s) =>
+    ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
+
+structure P = OuterParse and K = OuterSyntax.Keyword;
+
+val constdefsP =
+  OuterSyntax.command "constdefs" "declare and define constants (old style)"
+    K.thy_decl
+    (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o old_add_constdefs));
+
+in
+
+val _ = OuterSyntax.add_parsers [constdefsP];
+
+end;
+
 with_path ".." use_thy "HOL4Compat";
 with_path ".." use_thy "HOL4Syntax";
 setmp quick_and_dirty true use_thy "HOL4Prob";

--- a/src/HOL/Import/ROOT.ML	Thu Apr 22 11:01:34 2004 +0200
+++ b/src/HOL/Import/ROOT.ML	Thu Apr 22 11:02:22 2004 +0200
@@ -3,5 +3,30 @@
     Author:     Sebastian Skalberg (TU Muenchen)
 *)
 
+
+(* FIXME tmp hack to get generated theories work *)
+
+local
+
+fun old_add_constdefs args thy =
+  thy
+  |> Theory.add_consts (map fst args)
+  |> IsarThy.add_defs (false, map (fn ((c, _, mx), s) =>
+    ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
+
+structure P = OuterParse and K = OuterSyntax.Keyword;
+
+val constdefsP =
+  OuterSyntax.command "constdefs" "declare and define constants (old style)"
+    K.thy_decl
+    (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o old_add_constdefs));
+
+in
+
+val _ = OuterSyntax.add_parsers [constdefsP];
+
+end;
+
+
 use_thy "HOL4Compat";
 use_thy "HOL4Syntax";