equal
deleted
inserted
replaced
427 val n = Sign.arity_number thy tyco; |
427 val n = Sign.arity_number thy tyco; |
428 in |
428 in |
429 thy |
429 thy |
430 |> Class.prove_instance_arity (Class.intro_classes_tac []) |
430 |> Class.prove_instance_arity (Class.intro_classes_tac []) |
431 [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] [] |
431 [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] [] |
|
432 |> snd |
432 end |
433 end |
433 |
434 |
434 val (size_def_thms, thy') = |
435 val (size_def_thms, thy') = |
435 thy1 |
436 thy1 |
436 |> Theory.add_consts_i (map (fn (s, T) => |
437 |> Theory.add_consts_i (map (fn (s, T) => |