src/Tools/IsaPlanner/isand.ML
changeset 35845 e5980f0ad025
parent 31945 d5f186aa0bed
child 43324 2b47822868e4
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Sat Mar 20 02:23:41 2010 +0100
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Sat Mar 20 17:33:11 2010 +0100
     1.3 @@ -213,7 +213,7 @@
     1.4      let 
     1.5        val varfiytfrees = map (Term.dest_TFree o Thm.typ_of) ns
     1.6        val skiptfrees = subtract (op =) varfiytfrees (OldTerm.add_term_tfrees (Thm.prop_of th,[]));
     1.7 -    in #2 (Thm.varifyT' skiptfrees th) end;
     1.8 +    in #2 (Thm.varifyT_global' skiptfrees th) end;
     1.9  
    1.10  (* change schematic/meta vars to fresh free vars, avoiding name clashes 
    1.11     with "names" *)