src/HOL/Import/HOL/ROOT.ML
author wenzelm
Thu Apr 22 11:02:22 2004 +0200 (2004-04-22)
changeset 14652 5ddbdbadba06
parent 14620 1be590fd2422
child 14694 49873d345a39
permissions -rw-r--r--
tmp hack get back to old 'constdefs';
     1 (*  Title:      HOL/Import/HOL/ROOT.ML
     2     ID:         $Id$
     3     Author:     Sebastian Skalberg (TU Muenchen)
     4 *)
     5 
     6 (* FIXME tmp hack to get generated theories work *)
     7 
     8 local
     9 
    10 fun old_add_constdefs args thy =
    11   thy
    12   |> Theory.add_consts (map fst args)
    13   |> IsarThy.add_defs (false, map (fn ((c, _, mx), s) =>
    14     ((Thm.def_name (Syntax.const_name c mx), s), [])) args);
    15 
    16 structure P = OuterParse and K = OuterSyntax.Keyword;
    17 
    18 val constdefsP =
    19   OuterSyntax.command "constdefs" "declare and define constants (old style)"
    20     K.thy_decl
    21     (Scan.repeat1 (P.const -- P.term) >> (Toplevel.theory o old_add_constdefs));
    22 
    23 in
    24 
    25 val _ = OuterSyntax.add_parsers [constdefsP];
    26 
    27 end;
    28 
    29 with_path ".." use_thy "HOL4Compat";
    30 with_path ".." use_thy "HOL4Syntax";
    31 setmp quick_and_dirty true use_thy "HOL4Prob";
    32 setmp quick_and_dirty true use_thy "HOL4";