src/Pure/Isar/proof_context.ML

--- a/src/Pure/Isar/proof_context.ML	Sat May 01 22:09:45 2004 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat May 01 22:10:37 2004 +0200
@@ -157,19 +157,18 @@
     data: Object.T Symtab.table,                              (*user data*)
     asms:
       ((cterm list * exporter) list *                         (*assumes: A ==> _*)
-        (string * thm list) list) *
+        (string * thm list) list) *                           (*prems: A |- A *)
       (string * string) list,                                 (*fixes: !!x. _*)
-    (* CB: asms is of the form ((asms, prems), fixed) *)
     binds: (term * typ) option Vartab.table,                  (*term bindings*)
     thms: bool * NameSpace.T * thm list option Symtab.table
       * FactIndex.T,                                          (*local thms*)
-    (* CB: thms is of the form (q, n, t, i) where
+    (*thms is of the form (q, n, t, i) where
        q: indicates whether theorems with qualified names may be stored;
           this is initially forbidden (false); flag may be changed with
           qualified and restore_qualified;
        n: theorem namespace;
        t: table of theorems;
-       i: index for theorem lookup (find theorem command) *) 
+       i: index for theorem lookup (cf. thms_containing) *)
     cases: (string * RuleCases.T) list,                       (*local contexts*)
     defs:
       typ Vartab.table *                                      (*type constraints*)
@@ -304,31 +303,11 @@
 val fixedN = "\\<^fixed>";
 val structN = "\\<^struct>";
 
-fun the_struct structs i =
-  if 1 <= i andalso i <= length structs then Library.nth_elem (i - 1, structs)
-  else raise ERROR_MESSAGE ("Illegal reference to implicit structure #" ^ string_of_int i);
 
-
-(* parse translations *)
+(* translation functions *)
 
 fun fixed_tr x = (fixedN ^ x, curry Term.list_comb (Syntax.free x));
 
-fun index_tr struct_ (Const ("_noindex", _)) = Syntax.free (struct_ 1)
-  | index_tr struct_ (t as (Const ("_index", _) $ Const (s, _))) =
-      Syntax.free (struct_
-        (case Syntax.read_nat s of Some n => n | None => raise TERM ("index_tr", [t])))
-  | index_tr _ (Const ("_indexlogic", _) $ t) = t
-  | index_tr _ t = raise TERM ("index_tr", [t]);
-
-fun struct_tr structs [idx] = index_tr (the_struct structs) idx
-  | struct_tr _ ts = raise TERM ("struct_tr", ts);
-
-
-(* print (ast) translations *)
-
-fun index_tr' 1 = Syntax.const "_noindex"
-  | index_tr' i = Syntax.const "_index" $ Syntax.const (Library.string_of_int i);
-
 fun context_tr' ctxt =
   let
     val (_, structs, mixfixed) = syntax_of ctxt;
@@ -336,25 +315,14 @@
     fun tr' (t $ u) = tr' t $ tr' u
       | tr' (Abs (x, T, t)) = Abs (x, T, tr' t)
       | tr' (t as Free (x, T)) =
-          let val i = Library.find_index (equal x) structs + 1 in
-            if 1 <= i andalso i <= 9 then Syntax.const "_struct" $ index_tr' i
-            else if x mem_string mixfixed then Const (fixedN ^ x, T)
+          let val i = Library.find_index_eq x structs + 1 in
+            if i = 0 andalso x mem_string mixfixed then Const (fixedN ^ x, T)
+            else if i = 1 then Syntax.const "_struct" $ Syntax.const "_indexdefault"
             else t
           end
       | tr' a = a;
   in tr' end;
 
-fun index_ast_tr' structs s =
-  (case Syntax.read_nat s of
-    Some i => Syntax.Variable (the_struct structs i handle ERROR_MESSAGE _ => raise Match)
-  | None => raise Match);
-
-fun struct_ast_tr' structs [Syntax.Constant "_noindex"] =
-      index_ast_tr' structs "1"
-  | struct_ast_tr' structs [Syntax.Appl [Syntax.Constant "_index", Syntax.Constant s]] =
-      index_ast_tr' structs s
-  | struct_ast_tr' _ _ = raise Match;
-
 
 (* add syntax *)
 
@@ -391,8 +359,8 @@
     in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end)
 
 fun syn_of (Context {syntax = (syn, structs, _), ...}) =
-  syn |> Syntax.extend_trfuns
-    ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
+  syn |> Syntax.extend_trfuns (Syntax.struct_trfuns structs);
+
 
 end;
 
@@ -459,8 +427,8 @@
           (case env (x, ~1) of
               Some _ => t
             | None => (case lookup_skolem ctxt (no_skolem false ctxt x) of
-		  Some x' => Free (x', T)
-		| None => t))
+                  Some x' => Free (x', T)
+                | None => t))
       | intern (t $ u) = intern t $ intern u
       | intern (Abs (x, T, t)) = Abs (x, T, intern t)
       | intern a = a;
@@ -592,13 +560,13 @@
                   | Some (_, _, used'') => used @ used'';
   in
     (transform_error (read (syn_of ctxt)
-	(sign_of ctxt) (types', sorts', used')) s
+        (sign_of ctxt) (types', sorts', used')) s
       handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
       | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
     |> app (intern_skolem ctxt (case env_opt of None => K None | Some (env, _, _) => env))
     |> app (if is_pat then I else norm_term ctxt schematic allow_vars)
     |> app (if is_pat then prepare_dummies
-	 else if dummies then I else reject_dummies ctxt)
+         else if dummies then I else reject_dummies ctxt)
   end
 in