# HG changeset patch # User ballarin # Date 1227110400 -3600 # Node ID 6882e110c29ac64204910e68f8d6d3f3e1e12c57 # Parent 9458d7a6388a39e04d13b88e7f8f5126a0d4f948 Basic types not qualified. diff -r 9458d7a6388a -r 6882e110c29a src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Wed Nov 19 16:58:33 2008 +0100 +++ b/src/Pure/Isar/element.ML Wed Nov 19 17:00:00 2008 +0100 @@ -75,7 +75,7 @@ val generalize_facts: Proof.context -> Proof.context -> (Attrib.binding * (thm list * Attrib.src list) list) list -> (Attrib.binding * (thm list * Attrib.src list) list) list - val activate: (Term.typ, Term.term, Facts.ref) ctxt list -> Proof.context -> + val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> (context_i list * (Name.binding * Thm.thm list) list) * Proof.context val activate_i: context_i list -> Proof.context -> (context_i list * (Name.binding * Thm.thm list) list) * Proof.context