src/HOL/Import/HOL/ROOT.ML
changeset 14652 5ddbdbadba06
parent 14620 1be590fd2422
child 14694 49873d345a39
     1.1 --- a/src/HOL/Import/HOL/ROOT.ML	Thu Apr 22 11:01:34 2004 +0200
     1.2 +++ b/src/HOL/Import/HOL/ROOT.ML	Thu Apr 22 11:02:22 2004 +0200
     1.3 @@ -3,6 +3,29 @@
     1.4      Author:     Sebastian Skalberg (TU Muenchen)
     1.5  *)
     1.6  
     1.7 +(* FIXME tmp hack to get generated theories work *)
     1.8 +
     1.9 +local
    1.10 +
    1.11 +fun old_add_constdefs args thy =
    1.12 +  thy
    1.13 +  |> Theory.add_consts (map fst args)
    1.14 +  |> IsarThy.add_defs (false, map (fn ((c, _, mx), s) =>
    1.15 +    ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
    1.16 +
    1.17 +structure P = OuterParse and K = OuterSyntax.Keyword;
    1.18 +
    1.19 +val constdefsP =
    1.20 +  OuterSyntax.command "constdefs" "declare and define constants (old style)"
    1.21 +    K.thy_decl
    1.22 +    (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o old_add_constdefs));
    1.23 +
    1.24 +in
    1.25 +
    1.26 +val _ = OuterSyntax.add_parsers [constdefsP];
    1.27 +
    1.28 +end;
    1.29 +
    1.30  with_path ".." use_thy "HOL4Compat";
    1.31  with_path ".." use_thy "HOL4Syntax";
    1.32  setmp quick_and_dirty true use_thy "HOL4Prob";