tmp hack get back to old 'constdefs';
authorwenzelm
Thu Apr 22 11:02:22 2004 +0200 (2004-04-22)
changeset 146525ddbdbadba06
parent 14651 02b8f3bcf7fe
child 14653 0848ab6fe5fc
tmp hack get back to old 'constdefs';
src/HOL/Import/HOL/ROOT.ML
src/HOL/Import/ROOT.ML
     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";
     2.1 --- a/src/HOL/Import/ROOT.ML	Thu Apr 22 11:01:34 2004 +0200
     2.2 +++ b/src/HOL/Import/ROOT.ML	Thu Apr 22 11:02:22 2004 +0200
     2.3 @@ -3,5 +3,30 @@
     2.4      Author:     Sebastian Skalberg (TU Muenchen)
     2.5  *)
     2.6  
     2.7 +
     2.8 +(* FIXME tmp hack to get generated theories work *)
     2.9 +
    2.10 +local
    2.11 +
    2.12 +fun old_add_constdefs args thy =
    2.13 +  thy
    2.14 +  |> Theory.add_consts (map fst args)
    2.15 +  |> IsarThy.add_defs (false, map (fn ((c, _, mx), s) =>
    2.16 +    ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
    2.17 +
    2.18 +structure P = OuterParse and K = OuterSyntax.Keyword;
    2.19 +
    2.20 +val constdefsP =
    2.21 +  OuterSyntax.command "constdefs" "declare and define constants (old style)"
    2.22 +    K.thy_decl
    2.23 +    (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o old_add_constdefs));
    2.24 +
    2.25 +in
    2.26 +
    2.27 +val _ = OuterSyntax.add_parsers [constdefsP];
    2.28 +
    2.29 +end;
    2.30 +
    2.31 +
    2.32  use_thy "HOL4Compat";
    2.33  use_thy "HOL4Syntax";