# HG changeset patch
# User huffman
# Date 1284582381 25200
# Node ID d59b9531d6b06adced5adb169a218bea0d9ddd76
# Parent  16c53975ae1a0ec4232b5590e9b7ddb0a8ee3be2
remove code for obsolete 'fixpat' command

diff -r 16c53975ae1a -r d59b9531d6b0 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Wed Sep 15 12:54:17 2010 -0700
+++ b/src/HOLCF/Tools/fixrec.ML	Wed Sep 15 13:26:21 2010 -0700
@@ -10,8 +10,6 @@
     -> (Attrib.binding * term) list -> local_theory -> local_theory
   val add_fixrec_cmd: bool -> (binding * string option * mixfix) list
     -> (Attrib.binding * string) list -> local_theory -> local_theory
-  val add_fixpat: Thm.binding * term list -> theory -> theory
-  val add_fixpat_cmd: Attrib.binding * string list -> theory -> theory
   val add_matchers: (string * string) list -> theory -> theory
   val fixrec_simp_tac: Proof.context -> int -> tactic
   val setup: theory -> theory
@@ -409,34 +407,6 @@
 
 end; (* local *)
 
-(*************************************************************************)
-(******************************** Fixpat *********************************)
-(*************************************************************************)
-
-fun fix_pat thy t = 
-  let
-    val T = fastype_of t;
-    val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
-    val cname = case chead_of t of Const(c,_) => c | _ =>
-              fixrec_err "function is not declared as constant in theory";
-    val unfold_thm = Global_Theory.get_thm thy (cname^".unfold");
-    val simp = Goal.prove_global thy [] [] eq
-          (fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]);
-  in simp end;
-
-fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
-  let
-    val _ = legacy_feature "Old 'fixpat' command -- use \"fixrec_simp\" method instead";
-    val atts = map (prep_attrib thy) srcs;
-    val ts = map (prep_term thy) strings;
-    val simps = map (fix_pat thy) ts;
-  in
-    (snd o Global_Theory.add_thmss [((name, simps), atts)]) thy
-  end;
-
-val add_fixpat = gen_add_fixpat Sign.cert_term (K I);
-val add_fixpat_cmd = gen_add_fixpat Syntax.read_term_global Attrib.attribute;
-
 
 (*************************************************************************)
 (******************************** Parsers ********************************)
@@ -447,10 +417,6 @@
     ((Parse.opt_keyword "permissive" >> not) -- Parse.fixes -- Parse_Spec.where_alt_specs
       >> (fn ((strict, fixes), specs) => add_fixrec_cmd strict fixes specs));
 
-val _ =
-  Outer_Syntax.command "fixpat" "define rewrites for fixrec functions" Keyword.thy_decl
-    (Parse_Spec.specs >> (Toplevel.theory o add_fixpat_cmd));
-
 val setup =
   Method.setup @{binding fixrec_simp}
     (Scan.succeed (SIMPLE_METHOD' o fixrec_simp_tac))