src/HOLCF/Tools/cont_consts.ML
changeset 37098 b86d546c5282
parent 36960 01594f816e3a
child 40327 1dfdbd66093a
equal deleted inserted replaced
37097:476016cbf8b3 37098:b86d546c5282
    88 val add_consts = gen_add_consts Sign.certify_typ;
    88 val add_consts = gen_add_consts Sign.certify_typ;
    89 val add_consts_cmd = gen_add_consts Syntax.read_typ_global;
    89 val add_consts_cmd = gen_add_consts Syntax.read_typ_global;
    90 
    90 
    91 end;
    91 end;
    92 
    92 
    93 
       
    94 (* outer syntax *)
       
    95 
       
    96 val _ =
       
    97   Outer_Syntax.command "consts" "declare constants (HOLCF)" Keyword.thy_decl
       
    98     (Scan.repeat1 Parse.const_binding >> (Toplevel.theory o add_consts_cmd));
       
    99 
       
   100 end;
    93 end;