equal
deleted
inserted
replaced
587 (* wrapper -- restores quantifiers in rule specifications *) |
587 (* wrapper -- restores quantifiers in rule specifications *) |
588 fun inductive_def (binding as ((R, T), _)) intrs lthy = |
588 fun inductive_def (binding as ((R, T), _)) intrs lthy = |
589 let |
589 let |
590 val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) = |
590 val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, raw_induct, ...}, lthy) = |
591 lthy |
591 lthy |
592 |> Local_Theory.conceal |
592 |> Local_Theory.conceal |
593 |> Inductive.add_inductive_i |
593 |> Inductive.add_inductive_i |
594 {quiet_mode = true, |
594 {quiet_mode = true, |
595 verbose = ! trace, |
595 verbose = ! trace, |
596 alt_name = Binding.empty, |
596 alt_name = Binding.empty, |
597 coind = false, |
597 coind = false, |