1376 let |
1376 let |
1377 val thy = (ProofContext.theory_of lthy) |
1377 val thy = (ProofContext.theory_of lthy) |
1378 val const = prep_const thy raw_const |
1378 val const = prep_const thy raw_const |
1379 val nparams = get_nparams thy const |
1379 val nparams = get_nparams thy const |
1380 val intro_rules = pred_intros thy const |
1380 val intro_rules = pred_intros thy const |
1381 val (((tfrees, frees), fact), ctxt') = |
1381 val (((tfrees, frees), fact), lthy') = |
1382 Variable.import_thms true intro_rules lthy; |
1382 Variable.import_thms true intro_rules lthy; |
1383 val (pred, prop, ctxt'') = mk_casesrule fact nparams ctxt' |
1383 val (pred, prop, lthy'') = mk_casesrule fact nparams lthy' |
1384 val (predname, _) = dest_Const pred |
1384 val (predname, _) = dest_Const pred |
1385 fun after_qed [[th]] ctxt'' = |
1385 fun after_qed [[th]] lthy'' = |
1386 LocalTheory.note Thm.theoremK |
1386 LocalTheory.note Thm.theoremK |
1387 ((Binding.name (Long_Name.base_name predname ^ "_cases"), |
1387 ((Binding.name (Long_Name.base_name predname ^ "_cases"), (* FIXME: other suffix *) |
1388 [Attrib.internal (K (code_ind_cases_attrib))]) , [th]) ctxt'' |
1388 [Attrib.internal (K (code_ind_cases_attrib))]) , [th]) lthy'' |
1389 |> snd |
1389 |> snd |
1390 |> ProofContext.theory (create_def_equation predname) |
1390 |> LocalTheory.theory (create_def_equation predname) |
1391 in |
1391 in |
1392 Proof.theorem_i NONE after_qed [[(prop, [])]] ctxt'' |
1392 Proof.theorem_i NONE after_qed [[(prop, [])]] lthy'' |
1393 end; |
1393 end; |
1394 |
1394 |
1395 val code_pred = generic_code_pred (K I); |
1395 val code_pred = generic_code_pred (K I); |
1396 val code_pred_cmd = generic_code_pred Code_Unit.read_const |
1396 val code_pred_cmd = generic_code_pred Code_Unit.read_const |
1397 |
1397 |