src/Pure/variable.ML
changeset 20220 5dc68e9ecd9a
parent 20198 7b385487f22f
child 20240 a7b027328d6e
     1.1 --- a/src/Pure/variable.ML	Wed Jul 26 19:37:42 2006 +0200
     1.2 +++ b/src/Pure/variable.ML	Wed Jul 26 19:37:43 2006 +0200
     1.3 @@ -40,11 +40,12 @@
     1.4      (((indexname * sort) * typ) list * ((indexname * typ) * term) list) * Context.proof
     1.5    val importT_terms: term list -> Context.proof -> term list * Context.proof
     1.6    val import_terms: bool -> term list -> Context.proof -> term list * Context.proof
     1.7 -  val importT: thm list -> Context.proof -> thm list * Context.proof
     1.8 -  val import: bool -> thm list -> Context.proof -> thm list * Context.proof
     1.9 +  val importT: thm list -> Context.proof -> (ctyp list * thm list) * Context.proof
    1.10 +  val import: bool -> thm list -> Context.proof ->
    1.11 +    ((ctyp list * cterm list) * thm list) * Context.proof
    1.12    val tradeT: Context.proof -> (thm list -> thm list) -> thm list -> thm list
    1.13    val trade: Context.proof -> (thm list -> thm list) -> thm list -> thm list
    1.14 -  val focus: cterm -> Context.proof -> ((string * typ) list * cterm) * Context.proof
    1.15 +  val focus: cterm -> Context.proof -> (cterm list * cterm) * Context.proof
    1.16    val warn_extra_tfrees: Context.proof -> Context.proof -> unit
    1.17    val polymorphic: Context.proof -> term list -> term list
    1.18    val hidden_polymorphism: term -> typ -> (indexname * sort) list
    1.19 @@ -319,7 +320,7 @@
    1.20      val (instT, ctxt') = importT_inst (map Thm.full_prop_of ths) ctxt;
    1.21      val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
    1.22      val ths' = map (Thm.instantiate (instT', [])) ths;
    1.23 -  in (ths', ctxt') end;
    1.24 +  in ((map #2 instT', ths'), ctxt') end;
    1.25  
    1.26  fun import is_open ths ctxt =
    1.27    let
    1.28 @@ -330,13 +331,13 @@
    1.29      val instT' = map (fn (v, T) => (certT (TVar v), certT T)) instT;
    1.30      val inst' = map (fn (v, t) => (cert (Var v), cert t)) inst;
    1.31      val ths' = map (Thm.instantiate (instT', inst')) ths;
    1.32 -  in (ths', ctxt') end;
    1.33 +  in (((map #2 instT', map #2 inst'), ths'), ctxt') end;
    1.34  
    1.35  
    1.36  (* import/export *)
    1.37  
    1.38  fun gen_trade imp exp ctxt f ths =
    1.39 -  let val (ths', ctxt') = imp ths ctxt
    1.40 +  let val ((_, ths'), ctxt') = imp ths ctxt
    1.41    in exp ctxt' ctxt (f ths') end;
    1.42  
    1.43  val tradeT = gen_trade importT exportT;
    1.44 @@ -356,8 +357,8 @@
    1.45      val ps = Term.variant_frees t (Term.strip_all_vars t);   (*as they are printed :-*)
    1.46      val (xs, Ts) = split_list ps;
    1.47      val (xs', ctxt') = invent_fixes xs ctxt;
    1.48 -    val ps' = xs' ~~ Ts;
    1.49 -    val goal' = fold (forall_elim_prop o cert o Free) ps' goal;
    1.50 +    val ps' = ListPair.map (cert o Free) (xs', Ts);
    1.51 +    val goal' = fold forall_elim_prop ps' goal;
    1.52    in ((ps', goal'), ctxt') end;
    1.53  
    1.54