src/Pure/Isar/proof_context.ML
changeset 14508 859b11514537
parent 14287 f630017ed01c
child 14564 3667b4616e9a
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Apr 02 12:25:48 2004 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Apr 02 14:08:30 2004 +0200
     1.3 @@ -160,9 +160,17 @@
     1.4        ((cterm list * exporter) list *                         (*assumes: A ==> _*)
     1.5          (string * thm list) list) *
     1.6        (string * string) list,                                 (*fixes: !!x. _*)
     1.7 +    (* CB: asms is of the form ((asms, prems), fixed) *)
     1.8      binds: (term * typ) option Vartab.table,                  (*term bindings*)
     1.9      thms: bool * NameSpace.T * thm list option Symtab.table
    1.10        * FactIndex.T,                                          (*local thms*)
    1.11 +    (* CB: thms is of the form (q, n, t, i) where
    1.12 +       q: indicates whether theorems with qualified names may be stored;
    1.13 +          this is initially forbidden (false); flag may be changed with
    1.14 +          qualified and restore_qualified;
    1.15 +       n: theorem namespace;
    1.16 +       t: table of theorems;
    1.17 +       i: index for theorem lookup (find theorem command) *) 
    1.18      cases: (string * RuleCases.T) list,                       (*local contexts*)
    1.19      defs:
    1.20        typ Vartab.table *                                      (*type constraints*)
    1.21 @@ -1215,6 +1223,8 @@
    1.22  
    1.23  end;
    1.24  
    1.25 +(* CB: fix free variables occuring in ts, unless already fixed. *)
    1.26 +
    1.27  fun fix_frees ts ctxt =
    1.28    let
    1.29      val frees = foldl Term.add_frees ([], ts);