# HG changeset patch
# User bulwahn
# Date 1242027593 -7200
# Node ID 657386d94f14efd61203cf6fde21071e07aa8830
# Parent  9a1178204dc0b9f7465cf29ae7ae2904f87cf366
fixed code_pred command

diff -r 9a1178204dc0 -r 657386d94f14 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon May 11 09:18:42 2009 +0200
+++ b/etc/isar-keywords-ZF.el	Mon May 11 09:39:53 2009 +0200
@@ -45,15 +45,18 @@
     "class_deps"
     "classes"
     "classrel"
+    "codatatype"
     "code_datatype"
     "code_library"
     "code_module"
+    "coinductive"
     "commit"
     "constdefs"
     "consts"
     "consts_code"
     "context"
     "corollary"
+    "datatype"
     "declaration"
     "declare"
     "def"
@@ -83,6 +86,8 @@
     "help"
     "hence"
     "hide"
+    "inductive"
+    "inductive_cases"
     "init_toplevel"
     "instance"
     "instantiation"
@@ -118,6 +123,7 @@
     "presume"
     "pretty_setmargin"
     "prf"
+    "primrec"
     "print_abbrevs"
     "print_antiquotations"
     "print_ast_translation"
@@ -140,6 +146,7 @@
     "print_simpset"
     "print_statement"
     "print_syntax"
+    "print_tcset"
     "print_theorems"
     "print_theory"
     "print_trans_rules"
@@ -154,6 +161,7 @@
     "realizability"
     "realizers"
     "remove_thy"
+    "rep_datatype"
     "sect"
     "section"
     "setup"
@@ -207,9 +215,13 @@
     "attach"
     "begin"
     "binder"
+    "case_eqns"
+    "con_defs"
     "constrains"
     "contains"
     "defines"
+    "domains"
+    "elimination"
     "file"
     "fixes"
     "for"
@@ -217,17 +229,23 @@
     "if"
     "imports"
     "in"
+    "induction"
     "infix"
     "infixl"
     "infixr"
+    "intros"
     "is"
+    "monos"
     "notes"
     "obtains"
     "open"
     "output"
     "overloaded"
+    "recursor_eqns"
     "shows"
     "structure"
+    "type_elims"
+    "type_intros"
     "unchecked"
     "uses"
     "where"))
@@ -295,6 +313,7 @@
     "print_simpset"
     "print_statement"
     "print_syntax"
+    "print_tcset"
     "print_theorems"
     "print_theory"
     "print_trans_rules"
@@ -338,13 +357,16 @@
     "class"
     "classes"
     "classrel"
+    "codatatype"
     "code_datatype"
     "code_library"
     "code_module"
+    "coinductive"
     "constdefs"
     "consts"
     "consts_code"
     "context"
+    "datatype"
     "declaration"
     "declare"
     "defaultsort"
@@ -355,6 +377,7 @@
     "finalconsts"
     "global"
     "hide"
+    "inductive"
     "instantiation"
     "judgment"
     "lemmas"
@@ -371,11 +394,13 @@
     "overloading"
     "parse_ast_translation"
     "parse_translation"
+    "primrec"
     "print_ast_translation"
     "print_translation"
     "quickcheck_params"
     "realizability"
     "realizers"
+    "rep_datatype"
     "setup"
     "simproc_setup"
     "syntax"
@@ -390,7 +415,7 @@
     "use"))
 
 (defconst isar-keywords-theory-script
-  '())
+  '("inductive_cases"))
 
 (defconst isar-keywords-theory-goal
   '("corollary"
diff -r 9a1178204dc0 -r 657386d94f14 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon May 11 09:18:42 2009 +0200
+++ b/etc/isar-keywords.el	Mon May 11 09:39:53 2009 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace + HOL-ex.
+;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -36,6 +36,7 @@
     "atp_kill"
     "atp_messages"
     "attribute_setup"
+    "automaton"
     "ax_specification"
     "axclass"
     "axiomatization"
@@ -73,6 +74,7 @@
     "consts_code"
     "context"
     "corollary"
+    "cpodef"
     "datatype"
     "declaration"
     "declare"
@@ -84,6 +86,7 @@
     "defs"
     "disable_pr"
     "display_drafts"
+    "domain"
     "done"
     "enable_pr"
     "end"
@@ -97,6 +100,8 @@
     "find_consts"
     "find_theorems"
     "fix"
+    "fixpat"
+    "fixrec"
     "from"
     "full_prf"
     "fun"
@@ -146,6 +151,7 @@
     "overloading"
     "parse_ast_translation"
     "parse_translation"
+    "pcpodef"
     "pr"
     "prefer"
     "presume"
@@ -249,13 +255,15 @@
     "}"))
 
 (defconst isar-keywords-minor
-  '("advanced"
+  '("actions"
+    "advanced"
     "and"
     "assumes"
     "attach"
     "avoids"
     "begin"
     "binder"
+    "compose"
     "congs"
     "constrains"
     "contains"
@@ -263,6 +271,7 @@
     "file"
     "fixes"
     "for"
+    "hide_action"
     "hints"
     "identifier"
     "if"
@@ -271,7 +280,11 @@
     "infix"
     "infixl"
     "infixr"
+    "initially"
+    "inputs"
+    "internals"
     "is"
+    "lazy"
     "module_name"
     "monos"
     "morphisms"
@@ -279,10 +292,20 @@
     "obtains"
     "open"
     "output"
+    "outputs"
     "overloaded"
     "permissive"
+    "post"
+    "pre"
+    "rename"
+    "restrict"
     "shows"
+    "signature"
+    "states"
     "structure"
+    "to"
+    "transitions"
+    "transrel"
     "unchecked"
     "uses"
     "where"))
@@ -400,6 +423,7 @@
     "arities"
     "atom_decl"
     "attribute_setup"
+    "automaton"
     "axclass"
     "axiomatization"
     "axioms"
@@ -431,10 +455,13 @@
     "defer_recdef"
     "definition"
     "defs"
+    "domain"
     "equivariance"
     "extract"
     "extract_type"
     "finalconsts"
+    "fixpat"
+    "fixrec"
     "fun"
     "global"
     "hide"
@@ -487,6 +514,7 @@
   '("ax_specification"
     "code_pred"
     "corollary"
+    "cpodef"
     "function"
     "instance"
     "interpretation"
@@ -494,6 +522,7 @@
     "nominal_inductive"
     "nominal_inductive2"
     "nominal_primrec"
+    "pcpodef"
     "recdef_tc"
     "rep_datatype"
     "specification"
diff -r 9a1178204dc0 -r 657386d94f14 lib/jedit/isabelle.xml
--- a/lib/jedit/isabelle.xml	Mon May 11 09:18:42 2009 +0200
+++ b/lib/jedit/isabelle.xml	Mon May 11 09:39:53 2009 +0200
@@ -47,6 +47,7 @@
       <OPERATOR>ML_prf</OPERATOR>
       <LABEL>ML_val</LABEL>
       <OPERATOR>abbreviation</OPERATOR>
+      <KEYWORD4>actions</KEYWORD4>
       <KEYWORD4>advanced</KEYWORD4>
       <OPERATOR>also</OPERATOR>
       <KEYWORD4>and</KEYWORD4>
@@ -61,6 +62,7 @@
       <LABEL>atp_messages</LABEL>
       <KEYWORD4>attach</KEYWORD4>
       <OPERATOR>attribute_setup</OPERATOR>
+      <OPERATOR>automaton</OPERATOR>
       <KEYWORD4>avoids</KEYWORD4>
       <OPERATOR>ax_specification</OPERATOR>
       <OPERATOR>axclass</OPERATOR>
@@ -72,12 +74,14 @@
       <OPERATOR>by</OPERATOR>
       <INVALID>cannot_undo</INVALID>
       <KEYWORD2>case</KEYWORD2>
+      <KEYWORD4>case_eqns</KEYWORD4>
       <LABEL>cd</LABEL>
       <OPERATOR>chapter</OPERATOR>
       <OPERATOR>class</OPERATOR>
       <LABEL>class_deps</LABEL>
       <OPERATOR>classes</OPERATOR>
       <OPERATOR>classrel</OPERATOR>
+      <OPERATOR>codatatype</OPERATOR>
       <OPERATOR>code_abort</OPERATOR>
       <OPERATOR>code_class</OPERATOR>
       <OPERATOR>code_const</OPERATOR>
@@ -89,12 +93,15 @@
       <OPERATOR>code_module</OPERATOR>
       <OPERATOR>code_modulename</OPERATOR>
       <OPERATOR>code_monad</OPERATOR>
+      <OPERATOR>code_pred</OPERATOR>
       <OPERATOR>code_reserved</OPERATOR>
       <LABEL>code_thms</LABEL>
       <OPERATOR>code_type</OPERATOR>
       <OPERATOR>coinductive</OPERATOR>
       <OPERATOR>coinductive_set</OPERATOR>
       <LABEL>commit</LABEL>
+      <KEYWORD4>compose</KEYWORD4>
+      <KEYWORD4>con_defs</KEYWORD4>
       <KEYWORD4>congs</KEYWORD4>
       <OPERATOR>constdefs</OPERATOR>
       <KEYWORD4>constrains</KEYWORD4>
@@ -103,6 +110,7 @@
       <KEYWORD4>contains</KEYWORD4>
       <OPERATOR>context</OPERATOR>
       <OPERATOR>corollary</OPERATOR>
+      <OPERATOR>cpodef</OPERATOR>
       <OPERATOR>datatype</OPERATOR>
       <OPERATOR>declaration</OPERATOR>
       <OPERATOR>declare</OPERATOR>
@@ -115,7 +123,10 @@
       <OPERATOR>defs</OPERATOR>
       <LABEL>disable_pr</LABEL>
       <LABEL>display_drafts</LABEL>
+      <OPERATOR>domain</OPERATOR>
+      <KEYWORD4>domains</KEYWORD4>
       <OPERATOR>done</OPERATOR>
+      <KEYWORD4>elimination</KEYWORD4>
       <LABEL>enable_pr</LABEL>
       <KEYWORD3>end</KEYWORD3>
       <OPERATOR>equivariance</OPERATOR>
@@ -130,6 +141,8 @@
       <LABEL>find_theorems</LABEL>
       <KEYWORD2>fix</KEYWORD2>
       <KEYWORD4>fixes</KEYWORD4>
+      <OPERATOR>fixpat</OPERATOR>
+      <OPERATOR>fixrec</OPERATOR>
       <KEYWORD4>for</KEYWORD4>
       <OPERATOR>from</OPERATOR>
       <LABEL>full_prf</LABEL>
@@ -142,11 +155,13 @@
       <LABEL>help</LABEL>
       <OPERATOR>hence</OPERATOR>
       <OPERATOR>hide</OPERATOR>
+      <KEYWORD4>hide_action</KEYWORD4>
       <KEYWORD4>hints</KEYWORD4>
       <KEYWORD4>identifier</KEYWORD4>
       <KEYWORD4>if</KEYWORD4>
       <KEYWORD4>imports</KEYWORD4>
       <KEYWORD4>in</KEYWORD4>
+      <KEYWORD4>induction</KEYWORD4>
       <OPERATOR>inductive</OPERATOR>
       <KEYWORD1>inductive_cases</KEYWORD1>
       <OPERATOR>inductive_set</OPERATOR>
@@ -154,14 +169,19 @@
       <KEYWORD4>infixl</KEYWORD4>
       <KEYWORD4>infixr</KEYWORD4>
       <INVALID>init_toplevel</INVALID>
+      <KEYWORD4>initially</KEYWORD4>
+      <KEYWORD4>inputs</KEYWORD4>
       <OPERATOR>instance</OPERATOR>
       <OPERATOR>instantiation</OPERATOR>
+      <KEYWORD4>internals</KEYWORD4>
       <OPERATOR>interpret</OPERATOR>
       <OPERATOR>interpretation</OPERATOR>
+      <KEYWORD4>intros</KEYWORD4>
       <KEYWORD4>is</KEYWORD4>
       <OPERATOR>judgment</OPERATOR>
       <INVALID>kill</INVALID>
       <LABEL>kill_thy</LABEL>
+      <KEYWORD4>lazy</KEYWORD4>
       <OPERATOR>lemma</OPERATOR>
       <OPERATOR>lemmas</OPERATOR>
       <OPERATOR>let</OPERATOR>
@@ -193,12 +213,16 @@
       <KEYWORD4>open</KEYWORD4>
       <OPERATOR>oracle</OPERATOR>
       <KEYWORD4>output</KEYWORD4>
+      <KEYWORD4>outputs</KEYWORD4>
       <KEYWORD4>overloaded</KEYWORD4>
       <OPERATOR>overloading</OPERATOR>
       <OPERATOR>parse_ast_translation</OPERATOR>
       <OPERATOR>parse_translation</OPERATOR>
+      <OPERATOR>pcpodef</OPERATOR>
       <KEYWORD4>permissive</KEYWORD4>
+      <KEYWORD4>post</KEYWORD4>
       <LABEL>pr</LABEL>
+      <KEYWORD4>pre</KEYWORD4>
       <KEYWORD1>prefer</KEYWORD1>
       <KEYWORD2>presume</KEYWORD2>
       <LABEL>pretty_setmargin</LABEL>
@@ -228,6 +252,7 @@
       <LABEL>print_simpset</LABEL>
       <LABEL>print_statement</LABEL>
       <LABEL>print_syntax</LABEL>
+      <LABEL>print_tcset</LABEL>
       <LABEL>print_theorems</LABEL>
       <LABEL>print_theory</LABEL>
       <LABEL>print_trans_rules</LABEL>
@@ -244,19 +269,24 @@
       <OPERATOR>recdef</OPERATOR>
       <OPERATOR>recdef_tc</OPERATOR>
       <OPERATOR>record</OPERATOR>
+      <KEYWORD4>recursor_eqns</KEYWORD4>
       <LABEL>refute</LABEL>
       <OPERATOR>refute_params</OPERATOR>
       <LABEL>remove_thy</LABEL>
+      <KEYWORD4>rename</KEYWORD4>
       <OPERATOR>rep_datatype</OPERATOR>
+      <KEYWORD4>restrict</KEYWORD4>
       <OPERATOR>sect</OPERATOR>
       <OPERATOR>section</OPERATOR>
       <OPERATOR>setup</OPERATOR>
       <KEYWORD2>show</KEYWORD2>
       <KEYWORD4>shows</KEYWORD4>
+      <KEYWORD4>signature</KEYWORD4>
       <OPERATOR>simproc_setup</OPERATOR>
       <LABEL>sledgehammer</LABEL>
       <OPERATOR>sorry</OPERATOR>
       <OPERATOR>specification</OPERATOR>
+      <KEYWORD4>states</KEYWORD4>
       <OPERATOR>statespace</OPERATOR>
       <KEYWORD4>structure</KEYWORD4>
       <OPERATOR>subclass</OPERATOR>
@@ -278,11 +308,16 @@
       <LABEL>thm_deps</LABEL>
       <KEYWORD2>thus</KEYWORD2>
       <LABEL>thy_deps</LABEL>
+      <KEYWORD4>to</KEYWORD4>
       <LABEL>touch_thy</LABEL>
+      <KEYWORD4>transitions</KEYWORD4>
       <OPERATOR>translations</OPERATOR>
+      <KEYWORD4>transrel</KEYWORD4>
       <OPERATOR>txt</OPERATOR>
       <OPERATOR>txt_raw</OPERATOR>
       <LABEL>typ</LABEL>
+      <KEYWORD4>type_elims</KEYWORD4>
+      <KEYWORD4>type_intros</KEYWORD4>
       <OPERATOR>typed_print_translation</OPERATOR>
       <OPERATOR>typedecl</OPERATOR>
       <OPERATOR>typedef</OPERATOR>
diff -r 9a1178204dc0 -r 657386d94f14 src/HOL/ex/Predicate_Compile.thy
--- a/src/HOL/ex/Predicate_Compile.thy	Mon May 11 09:18:42 2009 +0200
+++ b/src/HOL/ex/Predicate_Compile.thy	Mon May 11 09:39:53 2009 +0200
@@ -49,6 +49,7 @@
 code_pred append
   using assms by (rule append.cases)
 
+thm append_codegen
 thm append_cases
 
 
diff -r 9a1178204dc0 -r 657386d94f14 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Mon May 11 09:18:42 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Mon May 11 09:39:53 2009 +0200
@@ -1378,18 +1378,18 @@
       val const = prep_const thy raw_const
       val nparams = get_nparams thy const
       val intro_rules = pred_intros thy const
-      val (((tfrees, frees), fact), ctxt') =
+      val (((tfrees, frees), fact), lthy') =
         Variable.import_thms true intro_rules lthy;
-      val (pred, prop, ctxt'') = mk_casesrule fact nparams ctxt'
+      val (pred, prop, lthy'') = mk_casesrule fact nparams lthy'
       val (predname, _) = dest_Const pred
-      fun after_qed [[th]] ctxt'' =
+      fun after_qed [[th]] lthy'' =
         LocalTheory.note Thm.theoremK
-          ((Binding.name (Long_Name.base_name predname ^ "_cases"),
-            [Attrib.internal (K (code_ind_cases_attrib))]) , [th]) ctxt''
+          ((Binding.name (Long_Name.base_name predname ^ "_cases"), (* FIXME: other suffix *)
+            [Attrib.internal (K (code_ind_cases_attrib))]) , [th]) lthy''
         |> snd
-        |> ProofContext.theory (create_def_equation predname)
+        |> LocalTheory.theory (create_def_equation predname)
     in
-      Proof.theorem_i NONE after_qed [[(prop, [])]] ctxt''
+      Proof.theorem_i NONE after_qed [[(prop, [])]] lthy''
     end;
 
   val code_pred = generic_code_pred (K I);