572 val _ = warning "defining type..."; |
572 val _ = warning "defining type..."; |
573 |
573 |
574 val (typedefs, thy6) = |
574 val (typedefs, thy6) = |
575 thy4 |
575 thy4 |
576 |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy => |
576 |> fold_map (fn (((name, mx), tvs), (cname, U)) => fn thy => |
577 Typedef.add_typedef_global |
577 Typedef.add_typedef_global false |
578 (name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *) |
578 (name, map (fn (v, _) => (v, dummyS)) tvs, mx) (* FIXME keep constraints!? *) |
579 (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $ |
579 (Const (@{const_name Collect}, (U --> HOLogic.boolT) --> HOLogic.mk_setT U) $ |
580 Const (cname, U --> HOLogic.boolT)) NONE |
580 Const (cname, U --> HOLogic.boolT)) NONE |
581 (rtac exI 1 THEN rtac CollectI 1 THEN |
581 (rtac exI 1 THEN rtac CollectI 1 THEN |
582 QUIET_BREADTH_FIRST (has_fewer_prems 1) |
582 QUIET_BREADTH_FIRST (has_fewer_prems 1) |