Nominal/nominal_atoms.ML
changeset 3135 92b9b8d2888d
parent 3045 d0ad264f8c4f
child 3193 87d1e815aa59
equal deleted inserted replaced
3134:301b74fcd614 3135:92b9b8d2888d
    74   in
    74   in
    75     thy
    75     thy
    76   end;
    76   end;
    77 
    77 
    78 (** outer syntax **)
    78 (** outer syntax **)
    79 
       
    80 local structure P = Parse and K = Keyword in
       
    81 
       
    82 val _ =
    79 val _ =
    83   Outer_Syntax.command "atom_decl" "declaration of a concrete atom type" K.thy_decl
    80   Outer_Syntax.command ("atom_decl", Keyword.thy_decl) 
    84     ((P.binding -- Scan.option (Args.parens (P.binding))) >>
    81     "declaration of a concrete atom type" 
    85       (Toplevel.print oo (Toplevel.theory o add_atom_decl)));
    82       ((Parse.binding -- Scan.option (Args.parens (Parse.binding))) >>
       
    83         (Toplevel.print oo (Toplevel.theory o add_atom_decl)))
    86 
    84 
    87 end;
    85 end;
    88 
       
    89 end;