# HG changeset patch
# User traytel
# Date 1365688991 -7200
# Node ID 876281e7642f23680ac21feaf635841326cfecaa
# Parent  6ae88642962f5e229a041059c46b57e31dc41a6e
installed case translations in BNF package

diff -r 6ae88642962f -r 876281e7642f src/HOL/BNF/Examples/Stream.thy
--- a/src/HOL/BNF/Examples/Stream.thy	Thu Apr 11 15:10:22 2013 +0200
+++ b/src/HOL/BNF/Examples/Stream.thy	Thu Apr 11 16:03:11 2013 +0200
@@ -30,9 +30,6 @@
         end
     *)
 *}
-translations -- "poor man's case syntax"
-  "case p of XCONST Stream x s \<Rightarrow> b" \<rightleftharpoons> "CONST stream_case (\<lambda>x s. b) p"
-  "case p of (XCONST Stream :: 'b) x s \<Rightarrow> b" \<rightharpoonup>" CONST stream_case (\<lambda>x s. b) p"
 
 code_datatype Stream
 lemmas [code] = stream.sels stream.sets stream.case
diff -r 6ae88642962f -r 876281e7642f src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 11 15:10:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Thu Apr 11 16:03:11 2013 +0200
@@ -112,7 +112,6 @@
     (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
-    (* TODO: case syntax *)
 
     val n = length raw_ctrs;
     val ks = 1 upto n;
@@ -639,7 +638,12 @@
           |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
       in
         ((discs, selss, exhaust_thm, inject_thms, distinct_thms, case_thms, disc_thmss, discI_thms,
-          sel_thmss), lthy |> Local_Theory.notes (notes' @ notes) |> snd)
+          sel_thmss),
+          lthy
+          |> Local_Theory.declaration {syntax = false, pervasive = true}
+             (fn phi => Case_Translation.register
+               (Morphism.term phi casex) (map (Morphism.term phi) ctrs))
+          |> Local_Theory.notes (notes' @ notes) |> snd)
       end;
   in
     (goalss, after_qed, lthy')