# HG changeset patch
# User wenzelm
# Date 1132941522 -3600
# Node ID 5ef79b75a002b1c9702a482eaecb200d9d1d98a2
# Parent  4a081083b06e64903a2642595c9b4678a4daa166
revert_skolem: fall back on Syntax.deskolem;

diff -r 4a081083b06e -r 5ef79b75a002 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Nov 25 18:58:41 2005 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Nov 25 18:58:42 2005 +0100
@@ -43,7 +43,7 @@
   val cert_typ_syntax: context -> typ -> typ
   val cert_typ_abbrev: context -> typ -> typ
   val get_skolem: context -> string -> string
-  val revert_skolem: context -> string -> string option
+  val revert_skolem: context -> string -> string
   val extern_skolem: context -> term -> term
   val read_termTs: context -> (string -> bool) -> (indexname -> typ option)
     -> (indexname -> sort option) -> string list -> (string * typ) list
@@ -437,13 +437,18 @@
 
 (* externalize Skolem constants -- approximation only! *)
 
-fun revert_skolem ctxt =
+fun rev_skolem ctxt =
   let val rev_fixes = map Library.swap (fixes_of ctxt)
   in AList.lookup (op =) rev_fixes end;
 
+fun revert_skolem ctxt x =
+  (case rev_skolem ctxt x of
+    SOME x' => x'
+  | NONE => Syntax.deskolem x);
+
 fun extern_skolem ctxt =
   let
-    val revert = revert_skolem ctxt;
+    val revert = rev_skolem ctxt;
     fun extern (t as Free (x, T)) =
         (case revert x of
           SOME x' => Free (if lookup_skolem ctxt x' = SOME x then x' else NameSpace.hidden x', T)
@@ -721,7 +726,7 @@
     val asms = Library.drop (length (assumptions_of outer), assumptions_of inner);
     val exp_asms = map (fn (cprops, exp) => exp is_goal cprops) asms;
   in
-    Goal.norm_hhf_protected
+    Goal.norm_hhf_protect
     #> Seq.EVERY (rev exp_asms)
     #> Seq.map (fn rule =>
       let
@@ -732,7 +737,7 @@
       in
         rule
         |> Drule.forall_intr_list frees
-        |> Goal.norm_hhf_protected
+        |> Goal.norm_hhf_protect
         |> Drule.tvars_intr_list tfrees |> #2
       end)
   end;