src/HOL/Mutabelle/mutabelle.ML

--- a/src/HOL/Mutabelle/mutabelle.ML	Wed Feb 13 13:38:52 2013 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Wed Feb 13 13:38:52 2013 +0100
@@ -30,9 +30,6 @@
       facts []
   end;
 
-fun thms_of thy = filter (fn (_, th) =>
-   Context.theory_name (theory_of_thm th) = Context.theory_name thy) (all_unconcealed_thms_of thy);
-
 fun consts_of thy =
  let
    val (namespace, const_table) = #constants (Consts.dest (Sign.consts_of thy))
@@ -128,8 +125,8 @@
  let 
    val revlC = rev longContext
    val revsC = rev shortContext
-   fun is_prefix [] longList = true
-     | is_prefix shList [] = false
+   fun is_prefix [] _ = true
+     | is_prefix _ [] = false
      | is_prefix (x::xs) (y::ys) = if (x=y) then is_prefix xs ys else false
  in 
    is_prefix revsC revlC
@@ -227,8 +224,8 @@
 (*evaluates if the two terms with paths passed as arguments can be exchanged, i.e. evaluates if one of the terms is a subterm of the other one*)  
 
 fun areReplacable [] [] = false
- | areReplacable fstPath [] = false
- | areReplacable [] sndPath = false
+ | areReplacable _ [] = false
+ | areReplacable [] _ = false
  | areReplacable (x::xs) (y::ys) = if (x=y) then areReplacable xs ys else true; 
 
 
@@ -237,21 +234,21 @@
 (*substitutes the term at the position of the first list in fstTerm by sndTerm. 
 The lists represent paths as generated by createSubTermList*)
 
-fun substitute [] fstTerm sndTerm = sndTerm
+fun substitute [] _ sndTerm = sndTerm
  | substitute (_::xs) (Abs(s,T,subTerm)) sndTerm = Abs(s,T,(substitute xs subTerm sndTerm))
  | substitute (0::xs) (t $ u) sndTerm = substitute xs t sndTerm $ u 
  | substitute (1::xs) (t $ u) sndTerm = t $ substitute xs u sndTerm
- | substitute (_::xs) _ sndTerm = 
+ | substitute (_::_) _ sndTerm = 
    raise WrongPath ("The Term could not be found at the specified position"); 
 
 
 (*get the subterm with the specified path in myTerm*)
 
 fun getSubTerm myTerm [] = myTerm
- | getSubTerm (Abs(s,T,subTerm)) (0::xs) = getSubTerm subTerm xs
- | getSubTerm (t $ u) (0::xs) = getSubTerm t xs
- | getSubTerm (t $ u) (1::xs) = getSubTerm u xs
- | getSubTerm _ (_::xs) = 
+ | getSubTerm (Abs(_,_,subTerm)) (0::xs) = getSubTerm subTerm xs
+ | getSubTerm (t $ _) (0::xs) = getSubTerm t xs
+ | getSubTerm (_ $ u) (1::xs) = getSubTerm u xs
+ | getSubTerm _ (_::_) = 
    raise WrongPath ("The subterm could not be found at the specified position");
 
 
@@ -423,23 +420,4 @@
      Free (if i = 0 then a else a ^ "_" ^ string_of_int i, T)
  | freeze t = t;
 
-fun inst_type insts (Type (s, Ts)) = Type (s, map (inst_type insts) Ts)
- | inst_type insts T = the_default HOLogic.intT (AList.lookup op = insts T);
-
-fun preprocess thy insts t = Object_Logic.atomize_term thy
- (map_types (inst_type insts) (freeze t));
-
-fun is_executable thy insts th =
-  let
-    val ctxt' = Proof_Context.init_global thy
-      |> Config.put Quickcheck.size 1
-      |> Config.put Quickcheck.iterations 1
-    val test = Quickcheck_Common.test_term
-      ("exhaustive", ((fn _ => raise (Fail "")), Exhaustive_Generators.compile_generator_expr)) ctxt' false
-  in  
-    case try test (preprocess thy insts (prop_of th), []) of
-      SOME _ => (Output.urgent_message "executable"; true)
-    | NONE => (Output.urgent_message ("not executable"); false)
-  end;                                               
-
 end