# HG changeset patch
# User haftmann
# Date 1135065516 -3600
# Node ID a1d53af4c4c79ed7de1f8fa16eaafe06e82da1a6
# Parent  b35d7312c64fb9aed030bda95814bd10f4df9c57
removed superfluos is_prefix functions

diff -r b35d7312c64f -r a1d53af4c4c7 src/HOL/Modelcheck/MuckeSyn.ML
--- a/src/HOL/Modelcheck/MuckeSyn.ML	Tue Dec 20 08:38:43 2005 +0100
+++ b/src/HOL/Modelcheck/MuckeSyn.ML	Tue Dec 20 08:58:36 2005 +0100
@@ -110,14 +110,10 @@
 
 local
 
-fun is_prefix [] s = true
-| is_prefix (p::ps) [] = false
-| is_prefix (p::ps) (x::xs) = (p=x) andalso (is_prefix ps xs);
-
 fun delete_bold [] = []
-| delete_bold (x::xs) = if (is_prefix ("\^["::"["::"0"::"m"::[]) (x::xs))
+| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
         then (let val (_::_::_::s) = xs in delete_bold s end)
-        else (if (is_prefix ("\^["::"["::"1"::"m"::[]) (x::xs))
+        else (if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
                 then  (let val (_::_::_::s) = xs in delete_bold s end)
                 else (x::delete_bold xs));
 
diff -r b35d7312c64f -r a1d53af4c4c7 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue Dec 20 08:38:43 2005 +0100
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue Dec 20 08:58:36 2005 +0100
@@ -523,7 +523,7 @@
 (* "true" stand at the end of the output.     *)
 local
 
-infix is_prefix_of contains at_post string_contains string_at_post;
+infix contains at_post string_contains string_at_post;
 
   val is_blank : string -> bool =
       fn " " => true | "\t" => true | "\n" => true | "\^L" => true 
@@ -537,13 +537,9 @@
   
   fun delete_blanks_string s = implode(delete_blanks (explode s));
 
-  fun [] is_prefix_of s = true
-    | (p::ps) is_prefix_of  [] = false
-    | (p::ps) is_prefix_of (x::xs) = (p = x) andalso (ps is_prefix_of xs);
-
   fun [] contains [] = true
     | [] contains s = false
-    | (x::xs) contains s = (s is_prefix_of (x::xs)) orelse (xs contains s);
+    | (x::xs) contains s = (is_prefix (op =) s (x::xs)) orelse (xs contains s);
 
   fun [] at_post [] = true
     | [] at_post s = false
diff -r b35d7312c64f -r a1d53af4c4c7 src/HOL/Tools/ATP/recon_parse.ML
--- a/src/HOL/Tools/ATP/recon_parse.ML	Tue Dec 20 08:38:43 2005 +0100
+++ b/src/HOL/Tools/ATP/recon_parse.ML	Tue Dec 20 08:58:36 2005 +0100
@@ -73,15 +73,12 @@
 
 
       exception NOCUT
-      fun is_prefix [] l = true
-        | is_prefix (h::t) [] = false
-        | is_prefix (h::t) (h'::t') = (h = h') andalso is_prefix t t'
       fun remove_prefix [] l = l
         | remove_prefix (h::t) [] = error "can't remove prefix"
         | remove_prefix (h::t) (h'::t') = remove_prefix t t'
       fun ccut t [] = raise NOCUT
         | ccut t s =
-            if is_prefix t s then ([], remove_prefix t s) else
+            if is_prefix (op =) t s then ([], remove_prefix t s) else
               let val (a, b) = ccut t (tl s) in ((hd s)::a, b) end
       fun cut t s =
         let
diff -r b35d7312c64f -r a1d53af4c4c7 src/HOLCF/IOA/Modelcheck/MuIOA.ML
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Tue Dec 20 08:38:43 2005 +0100
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML	Tue Dec 20 08:58:36 2005 +0100
@@ -94,14 +94,10 @@
 TransA sg t =
 error("malformed automaton def for TransA:\n" ^ (Sign.string_of_term sg t));
 
-fun is_prefix [] s = true
-| is_prefix (p::ps) [] = false
-| is_prefix (p::ps) (x::xs) = (p=x) andalso (is_prefix ps xs);
-
 fun delete_ul [] = []
-| delete_ul (x::xs) = if (is_prefix ("\^["::"["::"4"::"m"::[]) (x::xs))
+| delete_ul (x::xs) = if (is_prefix (op =) ("\^["::"["::"4"::"m"::[]) (x::xs))
         then (let val (_::_::_::s) = xs in delete_ul s end)
-        else (if (is_prefix ("\^["::"["::"0"::"m"::[]) (x::xs))
+        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
                 then  (let val (_::_::_::s) = xs in delete_ul s end)
                 else (x::delete_ul xs));
 
diff -r b35d7312c64f -r a1d53af4c4c7 src/HOLCF/IOA/meta_theory/ioa_package.ML
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Dec 20 08:38:43 2005 +0100
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Dec 20 08:58:36 2005 +0100
@@ -62,13 +62,10 @@
 fun extract_constrs thy [] = [] |
 extract_constrs thy (a::r) =
 let
-fun is_prefix [] s = true
-| is_prefix (p::ps) [] = false
-| is_prefix (p::ps) (x::xs) = (p=x) andalso (is_prefix ps xs);
 fun delete_bold [] = []
-| delete_bold (x::xs) = if (is_prefix ("\^["::"["::"1"::"m"::[]) (x::xs))
+| delete_bold (x::xs) = if (is_prefix (op =) ("\^["::"["::"1"::"m"::[]) (x::xs))
         then (let val (_::_::_::s) = xs in delete_bold s end)
-        else (if (is_prefix ("\^["::"["::"0"::"m"::[]) (x::xs))
+        else (if (is_prefix (op =) ("\^["::"["::"0"::"m"::[]) (x::xs))
                 then  (let val (_::_::_::s) = xs in delete_bold s end)
                 else (x::delete_bold xs));
 fun delete_bold_string s = implode(delete_bold(explode s));