# HG changeset patch
# User wenzelm
# Date 1083211368 -7200
# Node ID d796124e435cab780edc6ab24977c3ef0294296e
# Parent  2757b50f8f4814375add7fac7ff57174f92f8bbc
removed 'constdefs' hack;

diff -r 2757b50f8f48 -r d796124e435c src/HOL/Import/HOL/HOL4Base.thy
--- a/src/HOL/Import/HOL/HOL4Base.thy	Thu Apr 29 06:01:48 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Base.thy	Thu Apr 29 06:02:48 2004 +0200
@@ -2650,9 +2650,11 @@
 lemma MEMBER_NOT_EMPTY: "ALL x. (EX xa. IN xa x) = (x ~= EMPTY)"
   by (import pred_set MEMBER_NOT_EMPTY)
 
-constdefs
+consts
   UNIV :: "'a => bool" 
-  "pred_set.UNIV == %x. True"
+
+defs
+  UNIV_def: "pred_set.UNIV == %x. True"
 
 lemma UNIV_DEF: "pred_set.UNIV = (%x. True)"
   by (import pred_set UNIV_DEF)
@@ -2719,9 +2721,11 @@
 lemma PSUBSET_UNIV: "ALL x. PSUBSET x pred_set.UNIV = (EX xa. ~ IN xa x)"
   by (import pred_set PSUBSET_UNIV)
 
-constdefs
+consts
   UNION :: "('a => bool) => ('a => bool) => 'a => bool" 
-  "pred_set.UNION == %s t. GSPEC (%x. (x, IN x s | IN x t))"
+
+defs
+  UNION_def: "pred_set.UNION == %s t. GSPEC (%x. (x, IN x s | IN x t))"
 
 lemma UNION_DEF: "ALL s t. pred_set.UNION s t = GSPEC (%x. (x, IN x s | IN x t))"
   by (import pred_set UNION_DEF)
@@ -2761,9 +2765,11 @@
 lemma EMPTY_UNION: "ALL x xa. (pred_set.UNION x xa = EMPTY) = (x = EMPTY & xa = EMPTY)"
   by (import pred_set EMPTY_UNION)
 
-constdefs
+consts
   INTER :: "('a => bool) => ('a => bool) => 'a => bool" 
-  "pred_set.INTER == %s t. GSPEC (%x. (x, IN x s & IN x t))"
+
+defs
+  INTER_def: "pred_set.INTER == %s t. GSPEC (%x. (x, IN x s & IN x t))"
 
 lemma INTER_DEF: "ALL s t. pred_set.INTER s t = GSPEC (%x. (x, IN x s & IN x t))"
   by (import pred_set INTER_DEF)
diff -r 2757b50f8f48 -r d796124e435c src/HOL/Import/ROOT.ML
--- a/src/HOL/Import/ROOT.ML	Thu Apr 29 06:01:48 2004 +0200
+++ b/src/HOL/Import/ROOT.ML	Thu Apr 29 06:02:48 2004 +0200
@@ -3,30 +3,5 @@
     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";