# HG changeset patch
# User wenzelm
# Date 1134069370 -3600
# Node ID 99deeed095aed1bf8dc5075293dccd2b6fd481f1
# Parent  598e7fd7438bd316364831b4dcb53c1ffe985d2e
removed Syntax.deskolem;

diff -r 598e7fd7438b -r 99deeed095ae src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Dec 08 20:16:04 2005 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Dec 08 20:16:10 2005 +0100
@@ -434,7 +434,7 @@
 fun revert_skolem ctxt x =
   (case rev_skolem ctxt x of
     SOME x' => x'
-  | NONE => Syntax.deskolem x);
+  | NONE => perhaps (try Syntax.dest_skolem) x);
 
 fun extern_skolem ctxt =
   let
diff -r 598e7fd7438b -r 99deeed095ae src/Pure/Isar/rule_cases.ML
--- a/src/Pure/Isar/rule_cases.ML	Thu Dec 08 20:16:04 2005 +0100
+++ b/src/Pure/Isar/rule_cases.ML	Thu Dec 08 20:16:10 2005 +0100
@@ -162,7 +162,7 @@
 val case_hypsN = "hyps";
 val case_premsN = "prems";
 
-val strip_params = map (apfst Syntax.deskolem) o Logic.strip_params;
+val strip_params = map (apfst (perhaps (try Syntax.dest_skolem))) o Logic.strip_params;
 
 fun dest_binops cs tm =
   let
diff -r 598e7fd7438b -r 99deeed095ae src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Thu Dec 08 20:16:04 2005 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Thu Dec 08 20:16:10 2005 +0100
@@ -30,7 +30,6 @@
   val dest_internal: string -> string
   val skolem: string -> string
   val dest_skolem: string -> string
-  val deskolem: string -> string
   val read_nat: string -> int option
   val read_xnum: string -> IntInf.int
   val read_idents: string -> string list
@@ -356,7 +355,6 @@
 
 val skolem = suffix "__";
 val dest_skolem = unsuffix "__";
-fun deskolem x = the_default x (try dest_skolem x);
 
 
 (* read_nat *)
diff -r 598e7fd7438b -r 99deeed095ae src/Pure/drule.ML
--- a/src/Pure/drule.ML	Thu Dec 08 20:16:04 2005 +0100
+++ b/src/Pure/drule.ML	Thu Dec 08 20:16:10 2005 +0100
@@ -406,7 +406,7 @@
 fun outer_params t =
   let
     val vs = Term.strip_all_vars t;
-    val xs = Term.variantlist (map (Syntax.deskolem o #1) vs, []);
+    val xs = Term.variantlist (map (perhaps (try Syntax.dest_skolem) o #1) vs, []);
   in xs ~~ map #2 vs end;
 
 (*generalize outermost parameters*)