--- 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";