equal
deleted
inserted
replaced
390 val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]] |
390 val case_rhs = fold_rev (fold_rev Term.lambda) [fs, [u]] |
391 (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $ |
391 (Const (@{const_name The}, (B --> HOLogic.boolT) --> B) $ |
392 Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss))); |
392 Term.lambda w (Library.foldr1 HOLogic.mk_disj (map3 mk_case_disj xctrs xfs xss))); |
393 |
393 |
394 val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy |
394 val ((raw_case, (_, raw_case_def)), (lthy', lthy)) = no_defs_lthy |
395 |> Local_Theory.define ((case_binding, NoSyn), ((Thm.def_binding case_binding, []), case_rhs)) |
395 |> Local_Theory.define ((case_binding, NoSyn), |
|
396 ((Binding.conceal (Thm.def_binding case_binding), []), case_rhs)) |
396 ||> `Local_Theory.restore; |
397 ||> `Local_Theory.restore; |
397 |
398 |
398 val phi = Proof_Context.export_morphism lthy lthy'; |
399 val phi = Proof_Context.export_morphism lthy lthy'; |
399 |
400 |
400 val case_def = Morphism.thm phi raw_case_def; |
401 val case_def = Morphism.thm phi raw_case_def; |