src/Pure/Isar/typedecl.ML
changeset 56941 952833323c99
parent 56294 85911b8a6868
child 59970 e9f73d87d904
equal deleted inserted replaced
56940:35ce6dab3f5e 56941:952833323c99
    27 (* primitives *)
    27 (* primitives *)
    28 
    28 
    29 fun object_logic_arity name thy =
    29 fun object_logic_arity name thy =
    30   (case Object_Logic.get_base_sort thy of
    30   (case Object_Logic.get_base_sort thy of
    31     NONE => thy
    31     NONE => thy
    32   | SOME S => Axclass.axiomatize_arity (name, replicate (Sign.arity_number thy name) S, S) thy);
    32   | SOME S => Axclass.arity_axiomatization (name, replicate (Sign.arity_number thy name) S, S) thy);
    33 
    33 
    34 fun basic_decl decl (b, n, mx) lthy =
    34 fun basic_decl decl (b, n, mx) lthy =
    35   let val name = Local_Theory.full_name lthy b in
    35   let val name = Local_Theory.full_name lthy b in
    36     lthy
    36     lthy
    37     |> Local_Theory.background_theory (decl name)
    37     |> Local_Theory.background_theory (decl name)