# HG changeset patch
# User wenzelm
# Date 1177146462 -7200
# Node ID 5c1752279f25883b2a74b1668e29edb18f9b94e4
# Parent  f28f627546447ce9316c54d238d9eddf76880f05
added decode_term (belongs to Syntax module);

diff -r f28f62754644 -r 5c1752279f25 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Apr 21 01:34:15 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 21 11:07:42 2007 +0200
@@ -50,6 +50,7 @@
   val get_skolem: Proof.context -> string -> string
   val revert_skolem: Proof.context -> string -> string
   val revert_skolems: Proof.context -> term -> term
+  val decode_term: Proof.context -> term -> term
   val read_termTs: Proof.context -> (string -> bool) -> (indexname -> typ option)
     -> (indexname -> sort option) -> string list -> (string * typ) list
     -> term list * (indexname * typ) list
@@ -478,25 +479,38 @@
   handle TERM _ => error "Illegal dummy pattern(s) in term";
 
 
+(* decoding raw terms (syntax trees) *)
+
+fun legacy_intern_skolem ctxt internal def_type x =    (* FIXME cleanup this mess *)
+  let
+    val sko = lookup_skolem ctxt x;
+    val is_const = can (Consts.read_const (consts_of ctxt)) x;
+    val is_free = is_some sko orelse not is_const;
+    val is_internal = internal x;
+    val is_declared = is_some (def_type (x, ~1));
+    val res =
+      if is_free andalso not is_internal then (no_skolem false x; sko)
+      else ((no_skolem false x; ()) handle ERROR msg => warning msg;
+        if is_internal andalso is_declared then SOME x else NONE);
+  in if is_some res then res else if is_declared then SOME x else NONE end;
+
+fun decode_term ctxt =
+  let
+    val thy = theory_of ctxt;
+    val get_sort = Sign.get_sort thy (Variable.def_sort ctxt);
+    val map_const = try (#1 o Term.dest_Const o Consts.read_const (consts_of ctxt));
+    val map_free = legacy_intern_skolem ctxt (K false) (Variable.def_type ctxt false);
+    val map_type = Sign.intern_tycons thy;
+    val map_sort = Sign.intern_sort thy;
+  in Syntax.decode_term get_sort map_const map_free map_type map_sort end;
+
+
 (* read terms *)
 
 local
 
 fun append_env e1 e2 x = (case e2 x of NONE => e1 x | some => some);
 
-fun legacy_intern_skolem ctxt internal x =
-  let
-    val sko = lookup_skolem ctxt x;
-    val is_const = can (Consts.read_const (consts_of ctxt)) x;
-    val is_free = is_some sko orelse not is_const;
-    val is_internal = internal x;
-    val is_declared = is_some (Variable.default_type ctxt x);
-  in
-    if is_free andalso not is_internal then (no_skolem false x; sko)
-    else ((no_skolem false x; ()) handle ERROR msg => warning msg;
-      if is_internal andalso is_declared then SOME x else NONE)
-  end;
-
 fun gen_read' read app pattern schematic
     ctxt internal more_types more_sorts more_used s =
   let
@@ -504,7 +518,8 @@
     val sorts = append_env (Variable.def_sort ctxt) more_sorts;
     val used = fold Name.declare more_used (Variable.names_of ctxt);
   in
-    (read (pp ctxt) (syn_of ctxt) ctxt (types, sorts, used) (legacy_intern_skolem ctxt internal) s
+    (read (pp ctxt) (syn_of ctxt) ctxt (types, sorts, used)
+        (legacy_intern_skolem ctxt internal types) s
       handle TERM (msg, _) => error msg)
     |> app (certify_consts ctxt)
     |> app (if pattern then I else expand_binds ctxt schematic)