src/Pure/Proof/extraction.ML
changeset 26939 1035c89b4c02
parent 26653 60e0cf6bef89
child 27251 121991a4884d
     1.1 --- a/src/Pure/Proof/extraction.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -278,7 +278,7 @@
     1.4    let
     1.5      val {typeof_eqns, ...} = ExtractionData.get thy;
     1.6      fun err () = error ("Unable to determine type of extracted program for\n" ^
     1.7 -      Sign.string_of_term thy t)
     1.8 +      Syntax.string_of_term_global thy t)
     1.9    in case strip_abs_body (freeze_thaw (condrew thy (#net typeof_eqns)
    1.10      [typeof_proc (Sign.defaultS thy) vs]) (list_abs (map (pair "x") (rev Ts),
    1.11        Const ("typeof", fastype_of1 (Ts, t) --> Type ("Type", [])) $ t))) of
    1.12 @@ -582,7 +582,7 @@
    1.13              | SOME rs => (case find vs' rs of
    1.14                  SOME (_, prf') => (defs', prf_subst_TVars tye' prf')
    1.15                | NONE => error ("corr: no realizer for instance of theorem " ^
    1.16 -                  quote name ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
    1.17 +                  quote name ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
    1.18                      (Reconstruct.prop_of (proof_combt (prf0, ts))))))
    1.19            end
    1.20  
    1.21 @@ -596,7 +596,7 @@
    1.22              else case find vs' (Symtab.lookup_list realizers s) of
    1.23                SOME (_, prf) => (defs, prf_subst_TVars tye' prf)
    1.24              | NONE => error ("corr: no realizer for instance of axiom " ^
    1.25 -                quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
    1.26 +                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
    1.27                    (Reconstruct.prop_of (proof_combt (prf0, ts)))))
    1.28            end
    1.29  
    1.30 @@ -691,7 +691,7 @@
    1.31              | SOME rs => (case find vs' rs of
    1.32                  SOME (t, _) => (defs, subst_TVars tye' t)
    1.33                | NONE => error ("extr: no realizer for instance of theorem " ^
    1.34 -                  quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
    1.35 +                  quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
    1.36                      (Reconstruct.prop_of (proof_combt (prf0, ts))))))
    1.37            end
    1.38  
    1.39 @@ -703,7 +703,7 @@
    1.40              case find vs' (Symtab.lookup_list realizers s) of
    1.41                SOME (t, _) => (defs, subst_TVars tye' t)
    1.42              | NONE => error ("extr: no realizer for instance of axiom " ^
    1.43 -                quote s ^ ":\n" ^ Sign.string_of_term thy' (Envir.beta_norm
    1.44 +                quote s ^ ":\n" ^ Syntax.string_of_term_global thy' (Envir.beta_norm
    1.45                    (Reconstruct.prop_of (proof_combt (prf0, ts)))))
    1.46            end
    1.47