# HG changeset patch
# User blanchet
# Date 1346312866 -7200
# Node ID 640ce226a973896cc124d9a00bc36f72328199bc
# Parent  6b7cdb1f37d50e063ea6b0d04cc5726148235f6b
killed obsolete "bnf_of_typ" command

diff -r 6b7cdb1f37d5 -r 640ce226a973 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu Aug 30 09:47:46 2012 +0200
+++ b/etc/isar-keywords.el	Thu Aug 30 09:47:46 2012 +0200
@@ -35,7 +35,6 @@
     "bnf_codata"
     "bnf_data"
     "bnf_def"
-    "bnf_of_typ"
     "boogie_end"
     "boogie_open"
     "boogie_status"
@@ -471,7 +470,6 @@
     "axioms"
     "bnf_codata"
     "bnf_data"
-    "bnf_of_typ"
     "boogie_end"
     "boogie_open"
     "bundle"
diff -r 6b7cdb1f37d5 -r 640ce226a973 src/HOL/Codatatype/BNF_Comp.thy
--- a/src/HOL/Codatatype/BNF_Comp.thy	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Comp.thy	Thu Aug 30 09:47:46 2012 +0200
@@ -9,8 +9,6 @@
 
 theory BNF_Comp
 imports Basic_BNFs
-keywords
-  "bnf_of_typ" :: thy_decl
 uses
   "Tools/bnf_comp_tactics.ML"
   "Tools/bnf_comp.ML"
diff -r 6b7cdb1f37d5 -r 640ce226a973 src/HOL/Codatatype/Tools/bnf_comp.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp.ML	Thu Aug 30 09:47:46 2012 +0200
@@ -18,7 +18,6 @@
   val bnf_of_typ: BNF_Def.const_policy -> binding -> (binding -> binding) ->
     ((string * sort) list list -> (string * sort) list) -> typ -> unfold_thms * Proof.context ->
     (BNF_Def.BNF * (typ list * typ list)) * (unfold_thms * Proof.context)
-  val bnf_of_typ_cmd: binding * string -> Proof.context -> Proof.context
   val default_comp_sort: (string * sort) list list -> (string * sort) list
   val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
     (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_thms -> Proof.context ->
@@ -794,17 +793,4 @@
         end
     end;
 
-fun bnf_of_typ_cmd (b, rawT) lthy =
-  let
-    val ((bnf, (Ds, As)), (unfold, lthy')) =
-      bnf_of_typ Smart_Inline b I default_comp_sort (Syntax.read_typ lthy rawT)
-        (empty_unfold, lthy);
-  in
-    snd (seal_bnf unfold b Ds bnf lthy')
-  end;
-
-val _ =
-  Outer_Syntax.local_theory @{command_spec "bnf_of_typ"} "parse a type as composition of BNFs"
-    (((Parse.binding --| Parse.$$$ "=") -- Parse.typ) >> bnf_of_typ_cmd);
-
 end;
diff -r 6b7cdb1f37d5 -r 640ce226a973 src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Aug 30 09:47:46 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Thu Aug 30 09:47:46 2012 +0200
@@ -507,8 +507,7 @@
 val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false);
 
 fun user_policy ctxt =
-  if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms
-  else Derive_All_Facts_Note_Most;
+  if Config.get ctxt bnf_note_all then Note_All_Facts_and_Axioms else Derive_All_Facts_Note_Most;
 
 val smart_max_inline_size = 25; (*FUDGE*)