equal
deleted
inserted
replaced
2330 val nparams = nparams_of thy' const |
2330 val nparams = nparams_of thy' const |
2331 val intros = intros_of thy' const |
2331 val intros = intros_of thy' const |
2332 in mk_casesrule lthy' pred nparams intros end |
2332 in mk_casesrule lthy' pred nparams intros end |
2333 val cases_rules = map mk_cases preds |
2333 val cases_rules = map mk_cases preds |
2334 val cases = |
2334 val cases = |
2335 map (fn case_rule => RuleCases.Case {fixes = [], |
2335 map (fn case_rule => Rule_Cases.Case {fixes = [], |
2336 assumes = [("", Logic.strip_imp_prems case_rule)], |
2336 assumes = [("", Logic.strip_imp_prems case_rule)], |
2337 binds = [], cases = []}) cases_rules |
2337 binds = [], cases = []}) cases_rules |
2338 val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases |
2338 val case_env = map2 (fn p => fn c => (Long_Name.base_name p, SOME c)) preds cases |
2339 val lthy'' = lthy' |
2339 val lthy'' = lthy' |
2340 |> fold Variable.auto_fixes cases_rules |
2340 |> fold Variable.auto_fixes cases_rules |