# HG changeset patch
# User wenzelm
# Date 1394188481 -3600
# Node ID 51b342baecdad1c40556cab335fa73753b89cb6d
# Parent  7644d63e8c3fe77ba4787135cda8141fc2595a34
removed dead code;

diff -r 7644d63e8c3f -r 51b342baecda src/HOL/Statespace/distinct_tree_prover.ML
--- a/src/HOL/Statespace/distinct_tree_prover.ML	Fri Mar 07 10:22:27 2014 +0100
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Fri Mar 07 11:34:41 2014 +0100
@@ -77,14 +77,6 @@
   | x => x);
 
 
-fun index_tree (Const (@{const_name Tip}, _)) path tab = tab
-  | index_tree (Const (@{const_name Node}, _) $ l $ x $ _ $ r) path tab =
-      tab
-      |> Termtab.update_new (x, path)
-      |> index_tree l (path @ [Left])
-      |> index_tree r (path @ [Right])
-  | index_tree t _ _ = raise TERM ("index_tree: input not a tree", [t])
-
 fun split_common_prefix xs [] = ([], xs, [])
   | split_common_prefix [] ys = ([], [], ys)
   | split_common_prefix (xs as (x :: xs')) (ys as (y :: ys')) =
@@ -138,7 +130,6 @@
  *)
 fun naive_cterm_first_order_match (t, ct) env =
   let
-    val thy = theory_of_cterm ct;
     fun mtch (env as (tyinsts, insts)) =
       fn (Var (ixn, T), ct) =>
           (case AList.lookup (op =) insts ixn of
diff -r 7644d63e8c3f -r 51b342baecda src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Fri Mar 07 10:22:27 2014 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Fri Mar 07 11:34:41 2014 +0100
@@ -174,7 +174,7 @@
   Simplifier.simproc_global @{theory} "update_simp" ["update d c n v s"]
     (fn ctxt => fn t =>
       (case t of
-        ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s) =>
+        Const (@{const_name StateFun.update}, uT) $ _ $ _ $ _ $ _ $ _ =>
           let
             val (_ :: _ :: _ :: _ :: sT :: _) = binder_types uT;
               (*"('v => 'a1) => ('a2 => 'v) => 'n => ('a1 => 'a2) => ('n => 'v) => ('n => 'v)"*)
@@ -208,7 +208,7 @@
                 * updates again, the optimised term is constructed.
                 *)
             fun mk_updterm already
-                (t as ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s)) =
+                ((upd as Const (@{const_name StateFun.update}, uT)) $ d $ c $ n $ v $ s) =
                   let
                     fun rest already = mk_updterm already;
                     val (dT :: cT :: nT :: vT :: sT :: _) = binder_types uT;
@@ -238,7 +238,8 @@
                               Const (@{const_name StateFun.update},
                                 d'T --> c'T --> nT --> vT' --> sT --> sT);
                           in
-                            (upd $ d $ c $ n $ kb $ trm, upd' $ d' $ c' $ n $ f' $ trm', kv :: vars, comps', b)
+                            (upd $ d $ c $ n $ kb $ trm, upd' $ d' $ c' $ n $ f' $ trm', kv :: vars,
+                              comps', b)
                           end)
                   end
               | mk_updterm _ t = init_seed t;
diff -r 7644d63e8c3f -r 51b342baecda src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Fri Mar 07 10:22:27 2014 +0100
+++ b/src/HOL/Statespace/state_space.ML	Fri Mar 07 11:34:41 2014 +0100
@@ -78,16 +78,6 @@
 fun fold1' f [] x = x
   | fold1' f xs _ = fold1 f xs
 
-fun sublist_idx eq xs ys =
-  let
-    fun sublist n xs ys =
-         if is_prefix eq xs ys then SOME n
-         else (case ys of [] => NONE
-               | (y::ys') => sublist (n+1) xs ys')
-  in sublist 0 xs ys end;
-
-fun is_sublist eq xs ys = is_some (sublist_idx eq xs ys);
-
 fun sorted_subset eq [] ys = true
   | sorted_subset eq (x::xs) [] = false
   | sorted_subset eq (x::xs) (y::ys) = if eq (x,y) then sorted_subset eq xs ys
@@ -118,13 +108,6 @@
      {declinfo=declinfo,distinctthm=distinctthm,silent=silent};
 
 
-fun delete_declinfo n ctxt =
-  let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
-  in NameSpaceData.put
-       (make_namespace_data (Termtab.delete_safe n declinfo) distinctthm silent) ctxt
-  end;
-
-
 fun update_declinfo (n,v) ctxt =
   let val {declinfo,distinctthm,silent} = NameSpaceData.get ctxt;
   in NameSpaceData.put
@@ -252,7 +235,6 @@
   let
     val all_comps = parent_comps @ new_comps;
     val vars = (map (fn n => (Binding.name n, NONE, NoSyn)) all_comps);
-    val full_name = Sign.full_bname thy name;
     val dist_thm_name = distinct_compsN;
 
     val dist_thm_full_name = dist_thm_name;
@@ -296,7 +278,7 @@
     |> interprete_parent name dist_thm_full_name parent_expr
   end;
 
-fun encode_dot x = if x= #"." then #"_" else x;
+fun encode_dot x = if x = #"." then #"_" else x;
 
 fun encode_type (TFree (s, _)) = s
   | encode_type (TVar ((s,i),_)) = "?" ^ s ^ string_of_int i
@@ -309,23 +291,6 @@
 fun project_name T = projectN ^"_"^encode_type T;
 fun inject_name T = injectN ^"_"^encode_type T;
 
-fun project_free T pT V = Free (project_name T, V --> pT);
-fun inject_free T pT V = Free (inject_name T, pT --> V);
-
-fun get_name n = getN ^ "_" ^ n;
-fun put_name n = putN ^ "_" ^ n;
-fun get_const n T nT V = Free (get_name n, (nT --> V) --> T);
-fun put_const n T nT V = Free (put_name n, T --> (nT --> V) --> (nT --> V));
-
-fun lookup_const T nT V =
-  Const (@{const_name StateFun.lookup}, (V --> T) --> nT --> (nT --> V) --> T);
-
-fun update_const T nT V =
-  Const (@{const_name StateFun.update},
-    (V --> T) --> (T --> V) --> nT --> (T --> T) --> (nT --> V) --> (nT --> V));
-
-fun K_const T = Const (@{const_name K_statefun}, T --> T --> T);
-
 
 fun add_declaration name decl thy =
   thy
@@ -347,15 +312,12 @@
     val all_comps = rename renaming (parent_comps @ map (apsnd subst) components);
   in all_comps end;
 
-fun take_upto i xs = List.take(xs,i) handle General.Subscript => xs;
-
 fun statespace_definition state_type args name parents parent_comps components thy =
   let
     val full_name = Sign.full_bname thy name;
     val all_comps = parent_comps @ components;
 
     val components' = map (fn (n,T) => (n,(T,full_name))) components;
-    val all_comps' = map (fn (n,T) => (n,(T,full_name))) all_comps;
 
     fun parent_expr (prefix, (_, n, rs)) =
       (suffix namespaceN n, (prefix, Expression.Positional rs));
@@ -452,11 +414,6 @@
 
 (* prepare arguments *)
 
-fun read_raw_parent ctxt raw_T =
-  (case Proof_Context.read_typ_abbrev ctxt raw_T of
-    Type (name, Ts) => (Ts, name)
-  | T => error ("Bad parent statespace specification: " ^ Syntax.string_of_typ ctxt T));
-
 fun read_typ ctxt raw_T env =
   let
     val ctxt' = fold (Variable.declare_typ o TFree) env ctxt;
@@ -587,16 +544,15 @@
 (*** parse/print - translations ***)
 
 local
+
 fun map_get_comp f ctxt (Free (name,_)) =
       (case (get_comp ctxt name) of
         SOME (T,_) => f T T dummyT
       | NONE => (Syntax.free "arbitrary"(*; error "context not ready"*)))
   | map_get_comp _ _ _ = Syntax.free "arbitrary";
 
-val get_comp_projection = map_get_comp project_free;
-val get_comp_injection  = map_get_comp inject_free;
+fun name_of (Free (n,_)) = n;
 
-fun name_of (Free (n,_)) = n;
 in
 
 fun gen_lookup_tr ctxt s n =
@@ -624,7 +580,7 @@
           then Syntax.const "_statespace_lookup" $ s $ n
           else raise Match
       | NONE => raise Match)
-  | lookup_tr' _ ts = raise Match;
+  | lookup_tr' _ _ = raise Match;
 
 fun gen_update_tr id ctxt n v s =
   let